natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
basic constructions:
:
:
:
strong axioms
further
In type theory: the the natural numbers type is the type of natural numbers.
The type of natural numbers is the inductive type defined as follows.
See for instance (Pfenning, section 2).
In Coq-syntax the natural numbers are the inductive type defined by
Inductive nat : Type :=
| zero : nat
| succ : nat -> nat.
In the categorical semantics this is interpreted as the initial algebra for the endofunctor that sends an object to its coproduct with the terminal object
or in different equivalent notation, which is very suggestive here:
That initial algebra is (as explained there) precisely a natural number object . The two components of the morphism that defines the algebra structure are the 0-element and the successor endomorphism
In the following we write of course for short and .
We spell out in detail how the fact that satisfied def. is the classical induction principle.
That principle says informally that if a proposition depending on the natural numbers is true at and such that if it is true for some then it is true for , then it is true for all natural numbers.
Here is how this is formalized in type theory and then interpreted in some suitable ambient category .
First of all, that is a proposition depending on the natural numbers means that it is a dependent type
The categorical interpretation of this is by a display map
in the given category .
Next, the fact that holds at 0 means that there is a (proof-)term
In the categorical semantics the substitution of for 0 that gives is given by the pullback of the above fibration
and the term is interpreted as a section of the resultig fibration over the terminal object
But by the defining universal property of the pullback, this is equivalently just a commuting diagram
Next the induction step. Formally it says that for all there is an implication
The categorical semantics of the substitution of for is now given by the pullback
and the interpretation of the implication term is as a morphism in
Again by the universal property of the pullback this is the same as a commuting diagram
In summary this shows that the fact that is a proposition depending on natural numbers which holds at 0 and which holds at if it holds at is interpreted precisely as an -algebra homomorphism
The induction principle is supposed to deduce from this that holds for every , hence that there is a proof for all :
The categorical interpretation of this is as a morphism in . The existence of this is indeed exactly what the interpretation of the elimination rule, def. , gives, or (equivalently by prop. ) exactly what the initiality of the -algebra gives.
We spell out how the fact that satisfies def. is the classical recursion principle.
So let be an -algebra object, hence equipped with a morphism
and a morphism
By initiality of the -algebra , there is then a (unique) morphism
such that the diagram
commutes. This means precisely that is the function defined recursively by
;
.
Last revised on January 22, 2017 at 03:11:11. See the history of this page for a list of all contributions to it.