Changes

First, observe that the type of a ''tangent vector at a point'', also known as a ''directional derivative'' at that point, has the form <math>(\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K},</math> where <math>\mathbb{K}</math> is the chosen ground field, in the present case either <math>\mathbb{R}</math> or <math>\mathbb{B}.</math>  At a point in a space of type <math>\mathbb{K}^n,</math> a directional derivative operator <math>\vartheta\!</math> takes a function on that space, an <math>f\!</math> of type <math>(\mathbb{K}^n \to \mathbb{K}),</math> and maps it to a ground field value of type <math>\mathbb{K}.</math>  This value is known as the ''derivative'' of <math>f\!</math> in the direction <math>\vartheta\!</math> [Che46, 76&ndash;77].  In the boolean case <math>\vartheta  : (\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B}</math> has the form of a proposition about propositions, in other words, a proposition of the next higher type.

First, observe that the type of a ''tangent vector at a point'', also known as a ''directional derivative'' at that point, has the form <math>(\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K},</math> where <math>\mathbb{K}</math> is the chosen ground field, in the present case either <math>\mathbb{R}</math> or <math>\mathbb{B}.</math>  At a point in a space of type <math>\mathbb{K}^n,</math> a directional derivative operator <math>\vartheta\!</math> takes a function on that space, an <math>f\!</math> of type <math>(\mathbb{K}^n \to \mathbb{K}),</math> and maps it to a ground field value of type <math>\mathbb{K}.</math>  This value is known as the ''derivative'' of <math>f\!</math> in the direction <math>\vartheta\!</math> [Che46, 76&ndash;77].  In the boolean case <math>\vartheta  : (\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B}</math> has the form of a proposition about propositions, in other words, a proposition of the next higher type.

Next, by way of illustrating the propositions as types theme, consider a proposition of the form ''X''&nbsp;&rArr;&nbsp;(''Y''&nbsp;&rArr;&nbsp;''Z'').  One knows from propositional calculus that this is logically equivalent to a proposition of the form (''X''&nbsp;&and;&nbsp;''Y'')&nbsp;&rArr;&nbsp;''Z''.  But this equivalence should remind us of the functional isomorphism that exists between a construction of the type ''X''&nbsp;&rarr;&nbsp;(''Y''&nbsp;&rarr;&nbsp;''Z'') and a construction of the type (''X''&nbsp;&times;&nbsp;''Y'')&nbsp;&rarr;&nbsp;''Z''.  The propositions as types analogy permits us to take a functional type like this and, under the right conditions, replace the functional arrows "&rarr;" and products "&times;" with the respective logical arrows "&rArr;" and products "&and;".  Accordingly, viewing the result as a proposition, we can employ axioms and theorems of propositional calculus to suggest appropriate isomorphisms among the categorical and functional constructions.

Next, by way of illustrating the propositions as types idea, consider a proposition of the form <math>X \Rightarrow (Y \Rightarrow Z).</math> One knows from propositional calculus that this is logically equivalent to a proposition of the form <math>(X \land Y) \Rightarrow Z.</math> But this equivalence should remind us of the functional isomorphism that exists between a construction of the type <math>X \to (Y \to Z)</math> and a construction of the type <math>(X \times Y) \to Z.</math> The propositions as types analogy permits us to take a functional type like this and, under the right conditions, replace the functional arrows "<math>\to\!</math>" and products "<math>\times\!</math>" with the respective logical arrows "<math>\Rightarrow\!</math>" and products "<math>\land\!</math>".  Accordingly, viewing the result as a proposition, we can employ axioms and theorems of propositional calculus to suggest appropriate isomorphisms among the categorical and functional constructions.

Finally, examine the middle four rows of Table 3.  These display a series of isomorphic types that stretch from the categories that are labeled ''Vector Field'' to those that are labeled ''Derivation''.  A ''vector field'', also known as an ''infinitesimal transformation'', associates a tangent vector at a point with each point of a space.  In symbols, a vector field is a function of the form <math>\chi\!</math>&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;<math>\bigcup_x \ \chi_x\!</math> that assigns to each point ''x'' of the space ''X'' a tangent vector to ''X'' at that point, namely, the tangent vector <math>\chi_x\!</math> [Che46, 82-83].  If ''X'' is of type '''K'''^''n'', then <math>\chi\!</math> is of type '''K'''^''n''&nbsp;&rarr;&nbsp;(('''K'''^''n''&nbsp;&rarr;&nbsp;'''K''')&nbsp;&rarr;&nbsp;'''K''').  This has the pattern ''X''&nbsp;&rarr;&nbsp;(''Y''&nbsp;&rarr;&nbsp;''Z''), with ''X''&nbsp;=&nbsp;'''K'''^''n'', ''Y''&nbsp;=&nbsp;('''K'''^''n''&nbsp;&rarr;&nbsp;'''K'''), and ''Z''&nbsp;=&nbsp;'''K'''.

Finally, examine the middle four rows of Table&nbsp;3.  These display a series of isomorphic types that stretch from the categories that are labeled ''Vector Field'' to those that are labeled ''Derivation''.  A ''vector field'', also known as an ''infinitesimal transformation'', associates a tangent vector at a point with each point of a space.  In symbols, a vector field is a function of the form <math>\chi\!</math>&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;<math>\bigcup_x \ \chi_x\!</math> that assigns to each point ''x'' of the space ''X'' a tangent vector to ''X'' at that point, namely, the tangent vector <math>\chi_x\!</math> [Che46, 82&ndash;83].  If ''X'' is of type '''K'''^''n'', then <math>\chi\!</math> is of type '''K'''^''n''&nbsp;&rarr;&nbsp;(('''K'''^''n''&nbsp;&rarr;&nbsp;'''K''')&nbsp;&rarr;&nbsp;'''K''').  This has the pattern ''X''&nbsp;&rarr;&nbsp;(''Y''&nbsp;&rarr;&nbsp;''Z''), with ''X''&nbsp;=&nbsp;'''K'''^''n'', ''Y''&nbsp;=&nbsp;('''K'''^''n''&nbsp;&rarr;&nbsp;'''K'''), and ''Z''&nbsp;=&nbsp;'''K'''.

Applying the propositions as types analogy, one can follow this pattern through a series of metamorphoses from the type of a vector field to the type of a derivation, as traced out in Table 4.  Observe how the function ''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''K''', associated with the place of ''Y'' in the pattern, moves through its paces from the second to the first position.  In this way, the vector field <math>\chi\!</math>, initially viewed as attaching each tangent vector <math>\chi_x\!</math> to the site ''x'' where it acts in ''X'', now comes to be seen as acting on each scalar potential ''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''K''' like a generalized species of differentiation, producing another function <math>\chi\!</math>''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''K''' of the same type.

Applying the propositions as types analogy, one can follow this pattern through a series of metamorphoses from the type of a vector field to the type of a derivation, as traced out in Table 4.  Observe how the function ''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''K''', associated with the place of ''Y'' in the pattern, moves through its paces from the second to the first position.  In this way, the vector field <math>\chi\!</math>, initially viewed as attaching each tangent vector <math>\chi_x\!</math> to the site ''x'' where it acts in ''X'', now comes to be seen as acting on each scalar potential ''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''K''' like a generalized species of differentiation, producing another function <math>\chi\!</math>''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''K''' of the same type.