natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
= + +
/ | -/ | |
, | ||
of / of | ||
for | for hom-tensor adjunction | |
introduction rule for | for hom-tensor adjunction | |
( of) | ( of) | |
into | into | |
( of) | ( of) | |
, , | ||
higher | ||
/ | -// | |
/ | ||
, () | , | |
(, ) | / | |
(absence of) | (absence of) | |
An inductive type is…
In terms of categorical semantics, an inductive type is a type whose interpretation is given by an initial algebra of an endofunctor.
This has the usual meaning in ordinary category theory. In applications to (∞,1)-category theory, the uniqueness clause in the notion of initial object is modified to allow for a contractible space of choices (as discussed at initial object in an (∞,1)-category), and this difference is reflected accordingly in the type-theoretic set-up. The syntax will give back the traditional meaning whenever equality is interpreted extensionally.
There are two equivalent ways of defining the judgement rules for inductive types. The first describes elimination on dependent types over the given type. This is the formalization of the notion of induction, and discussed below in
The second describes elimination on absolute types. This is the formalization of the notion of recursion, and discussed below
(…)
(…)
We discuss the categorical semantics of inductive types.
The categorical interpretation of induction, hence of the dependent elimination and computation rules from above are the following.
Let $\mathcal{C}$ be the ambient category.
The interpretation of inductive term introduction is by an endofunctor $F : \mathcal{C} \to \mathcal{C}$ and an algebra over an endofunctor, exhibited by a morphism in $\mathcal{C}$ of the form
The interpretation of the dependent elimination rule says that given a display map $B \to W$, where $B$ is given an $F$-algebra structure and the display map is an $F$-algebra homomorphism, the dependent eliminator is interpreted as a specified section $\sigma : W \to B \in \mathcal{C}_{/W}$, hence as a diagram
in $\mathcal{C}$.
The interpretation of the dependent computation rules is that the section $\sigma$ from above is required to be an algebra homomorphism.
The categorical interpretation of recursion, hence of the absolute elimination rules from above in a suitable category $\mathcal{C}$ is the following
The interpretation of inductive term introduction is by an endofunctor $F : \mathcal{C} \to \mathcal{C}$ and an algebra over an endofunctor, exhibited by a morphism in $\mathcal{C}$ of the form
The interpretation of the absolute elimination rule is that for $A$ any other $F$-algebra, there is a morphism $W \to A$ in $\mathcal{C}$.
The interpretation of the absolute computation rule says that the morphism $W \to A$ from above is an algebra homomorphism and is unique as such.
In summary this says that the recursion rules are interpreted as an initial algebra of an endofunctor.
When interpreted in a category $\mathcal{C}$ of homotopy 0-types = sets, definition and definition are indeed equivalent.
First suppose that $W$ is an initial $F$-algebra as in def. . Then since initiality entails first of all the existence of a morphims to any other object it follows that with $B$ another $F$-algebra there is a homomorphism $W \to B$, and since secondly initiality entails uniqueness of this morphism, it follows that given a homomorphism $B \to W$ the composite $W \to B \to W$ has to equal the identity $id_W$, hence that $B \to W$ has a section, and uniquely so.
Conversely, assume that $W$ satisfies definition . For $A$ any other $F$-algebra we can form the trivial display map $W \times A \to W$ by projection and a section of this is equivalently just a morphism $W \to A$, so we have a homomorphism from $W$ to any other $F$-algebra $A$. Therefore to show that $W$ is an initial $F$-algebra it remains to show that for $f, g : W \to A$ two algebra homomorphism, they are necessarily equal.
To that end, notice that by the assumption of 0-truncation, the diagonal $\delta \colon A \to A \times A$ is a display map / fibration.
Form its pullback $P$
which is also an algebra homomorphism. Therefore by the interpretation of the elimination rule it has a (specified) section $\sigma : W \to P$. But $P \to W$ is the pullback of a monomorphism and therefore itself a monomorphism, and so the section forces it to be in fact an isomorphism. This in turn means that $f$ and $g$ are equal.
In intensional type theory, where the diagonal is not a display map, we can perform the same argument using a path object $P A \to A \times A$ (represented in type theory by an identity type), showing thereby that $f$ and $g$ are homotopic. A fancier version of this argument enables us to show that the space of algebra maps $W\to A$ is actually contractible. In other words, the axioms for an inductive type still imply that algebra maps out of $W$ are essentially unique, even though the axioms do not state this explicitly.
Any inductive type $W$ is a homotopy initial F-algebra: the space of $F$-algebra maps $W \to X$ is contractible.
The type of natural numbers $\mathbb{N}$ is the inductive type defined as follows.
(check, this probably still has syntax errors…)
(…)
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 $F$ 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 $\mathbb{N}$. The two components of the morphism $F(\mathbb{N}) \to \mathbb{N}$ that defines the algebra structure are the 0-element $zero : * \to \mathbb{N}$ and the successor endomorphism $successor : \mathbb{N} \to \mathbb{N}$
In the following we write of course for short $0 : * \to \mathbb{N}$ and $s : \mathbb{N} \to \mathbb{N}$.
We spell out in detail how the fact that $\mathbb{N}$ satisfied def. is the classical induction principle.
That principle says informally that if a proposition $P$ depending on the natural numbers is true at $n = 0$ and such that if it is true for some $n$ then it is true for $n+1$, 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 $\mathcal{C}$.
First of all, that $P$ 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 $\mathcal{C}$.
Next, the fact that $P$ holds at 0 means that there is a (proof-)term
In the categorical semantics the substitution of $n$ for 0 that gives $P(0)$ is given by the pullback of the above fibration
and the term $p_0$ 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 $n \in \mathbb{N}$ there is an implication $p_s(n) : P(n) \to P(n+1)$
The categorical semantics of the substitution of $n+1$ for $n$ is now given by the pullback
and the interpretation of the implication term $p_s(n)$ is as a morphism $P \to s^* P$ in $\mathcal{C}_{/\mathbb{N}}$
Again by the universal property of the pullback this is the same as a commuting diagram
In summary this shows that the fact that $P$ is a proposition depending on natural numbers which holds at 0 and which holds at $n+1$ if it holds at $n$ is interpreted precisely as an $F$-algebra homomorphism
The induction principle is supposed to deduce from this that $P$ holds for every $n$, hence that there is a proof $p_n : P(n)$ for all $n$:
The categorical interpretation of this is as a morphism $p : \mathbb{N} \to P$ in $\mathcal{C}_{/\mathbb{N}}$. 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 $F$-algebra $\mathbb{N}$ gives.
We spell out how the fact that $\mathbb{N}$ satisfies def. is the classical recursion principle.
So let $A$ be an $F$-algebra object, hence equipped with a morphism
and a morphism
By initiality of the $F$-algebra $\mathbb{N}$, there is then a (unique) morphism
such that the diagram
commutes. This means precisely that $f$ is the function defined recursively by
$f(0) = a_0$;
$f(n+1) = h(f(n))$.
The introduction, elimination and computation rules for identity types are discussed there.
In Coq-syntax the identity types are the inductive types (or more precisely, the inductive family) defined by
Inductive id {A} : A -> A -> Type :=
idpath : forall x, id x x.
We may interpret identity types in suitable categories $\mathcal{C}$ such as a type-theoretic model category.
The categorical interpretation of identity types in a category $\mathcal{C}$ is as the initial algebra for the endofunctor
of the slice category $\mathcal{C}_{/A \times A}$ over $A\times A$ which is constant at the diagonal $A\to A\times A$:
So an algebra for this endofunctor is a morphism
and the initial such is the path space object $A^I \to A \times A$.
We spell out in detail how the the induction principle def. for identity types is the principle of substitution of equals for equals.
To have an $F$-algebra $\langle E \to A\times A\rangle$ over $\langle A^I \to A \times A\rangle$ means precisely to have a diagram
in $\mathcal{C}$.
This is the interpretation of the elimination rule: $E \to A^I$ is the interpretation of a type
and the lift $A \to E$ is a section of the pullback of $E$ to $A$, hence an interpretation of a term in the substitution
The elimination rule then says that this extends to a section $A^I \to E$, hence a “proof of $E$ over all identifications” $a = b$.
We spell out how the the recursion principle def. for identity types is related to the Segal-completeness condition and in particular to univalence.
Notice that an algebra over the endofunctor that defines identity types, example ,
constitutes the 1-skeleton of a simplicial object
The recursion principle says that the degeneracy map $\sigma_0$ factors through the path space object of $X_0$ as a lift $\hat \sigma_0$ in the diagram
Semantically, this lift exists because $X_0 \to X_0^I$ is an acyclic cofibration by definition of path space object, and $X_1 \to X_0 \times X_0$ is a fibration (display map) by the interpretation rule for dependent types.
This morphism
lifts paths/morphisms that exist in $X_0$ to the morphisms exhibited by $X_1$, if we think of the above as the 1-skeleton of a simplicial object that represents an internal category in an (infinity,1)-category.
Suppose this exists, then there will be a notion of equivalences in $X_1$, those morphisms that are invertible with respect to the given composition operation. In good situations this will give the core inclusion
In this case the Segal-completeness condition in degree 1 says that the path recursion $\hat \sigma_0$ exhibits this inclusion
In the case that $X_\bullet$ is the classifier of the codomain fibration, then this is called the univalence-condition.
inductive type, initial algebra of an endofunctor
higher inductive type, initial algebra of a presentable ∞-monad
A very basic introduction to the concept, with an eye towards explaining identity types is in
A textbook account in the context of programming languages is in section 15 of
Discussion of inductive types in the context of Coq-programming is in chapter 3 of
See also
Expositions with an eye towards higher inductive types include
Mike Shulman, Homotopy type theory IV (web)
Peter LeFanu Lumsdaine, Higher inductive types, a tour of the menageries (blog post)
Mike Shulman, Inductive and higher inductive types, talk slides (2012) (pdf)
Original references include
The formalization in Coq is discussed in
A study of the homotopy-initiality of inductive types in homotopy type theory is in
The corresponding Coq-code is at
Exposition and discussion of that result is in
Discussion of the inductive type of natural numbers is in
Discussion of inductive types in the context of linear type theory is in
Last revised on April 29, 2018 at 06:18:42. See the history of this page for a list of all contributions to it.