Changes

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.

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&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 : X \to \bigcup_{x \in X} \chi_x</math> that assigns to each point <math>x\!</math> of the space <math>X\!</math> a tangent vector to <math>X\!</math> at that point, namely, the tangent vector <math>\chi_x\!</math> [Che46, 82&ndash;83].  If <math>X\!</math> is of type <math>\mathbb{K}^n,</math> then <math>\chi\!</math> is of type <math>\mathbb{K}^n \to ((\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K}).</math>  This has the pattern <math>X \to (Y \to Z),</math> with <math>X = \mathbb{K}^n,</math> <math>Y = (\mathbb{K}^n \to \mathbb{K}),</math> and <math>Z = \mathbb{K}.</math>

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>\xi : X \to \bigcup_{x \in X} \xi_x</math> that assigns to each point <math>x\!</math> of the space <math>X\!</math> a tangent vector to <math>X\!</math> at that point, namely, the tangent vector <math>\xi_x\!</math> [Che46, 82&ndash;83].  If <math>X\!</math> is of type <math>\mathbb{K}^n,</math> then <math>\xi\!</math> is of type <math>\mathbb{K}^n \to ((\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K}).</math>  This has the pattern <math>X \to (Y \to Z),</math> with <math>X = \mathbb{K}^n,</math> <math>Y = (\mathbb{K}^n \to \mathbb{K}),</math> and <math>Z = \mathbb{K}.</math>

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&nbsp;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&nbsp;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>\xi,\!</math> initially viewed as attaching each tangent vector <math>\xi_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>\xi\!</math>''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''K''' of the same type.

<font face="courier new">

<font face="courier new">