Changes

I think it's best to begin with a few simple observations, as I frequently find it necessary to return to the basics again and again, even if I take a different path each time.

I think it's best to begin with a few simple observations, as I frequently find it necessary to return to the basics again and again, even if I take a different path each time.

;Observation 1

: If we have the information that an element <math>x\!</math> is constrained to be of the type <math>X\!</math>

! Observation 1

: and we have the information that a function <math>f\!</math> is constrained to be of the type <math>X \to Y</math>

: then we have the information that the element <math>f(x)\!</math> is constrained to be of the type <math>Y.\!</math>

| '''IF''' we know that the element <math>x\!</math> is of the type <math>X\!</math>

| '''AND''' we know that the function <math>f\!</math> is of the type <math>X \to Y</math>

| '''THEN''' we know that the element <math>f(x)\!</math> is of the type <math>Y.\!</math>

We can abbreviate this inference, that operates on two pieces of information to produce another piece of information, in the following conventional form:

We can abbreviate this inference, that operates on two pieces of information to produce another piece of information, in the following conventional form: