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 ('''K'''^''n''&nbsp;&rarr; '''K''')&nbsp;&rarr;&nbsp;'''K''', where '''K''' is the chosen ground field, in the present case either '''R''' or '''B'''.  At a point in a space of type '''K'''^''n'', a directional derivative operator <math>\vartheta\!</math> takes a function on that space, an ''f'' of type ('''K'''^''n''&nbsp;&rarr; '''K'''), and maps it to a ground field value of type '''K'''.  This value is known as the ''derivative'' of ''f'' in the direction <math>\vartheta\!</math> [Che46, 76-77].  In the boolean case, <math>\vartheta\!</math>&nbsp;:&nbsp;('''B'''^''n''&nbsp;&rarr; '''B''')&nbsp;&rarr;&nbsp;'''B''' 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 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.