inductive type (changes) in nLab
- ️Sun Dec 01 2019
Showing changes from revision #50 to #51: Added | Removed | Changed
Context
Deduction and Induction
Type theory
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = \linebreak propositions as types +programs as proofs +relation type theory/category theory
Induction
Contents
Idea
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.
Definition
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
Induction: dependent elimination, computation
(…)
Recursion: elimination, computation
(…)
Categorical semantics
We discuss the categorical semantics of inductive types.
Definition
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:𝒞→𝒞F : \mathcal{C} \to \mathcal{C} and an algebra over an endofunctor, exhibited by a morphism in 𝒞\mathcal{C} of the form
F(W)→W. F(W) \to W \,.
-
The interpretation of the dependent elimination rule says that given a display map B→WB \to W, where BB is given an FF-algebra structure and the display map is an FF-algebra homomorphism, the dependent eliminator is interpreted as a specified section σ:W→B∈𝒞 /W\sigma : W \to B \in \mathcal{C}_{/W}, hence as a commuting diagram of the form
W ⟶σ B id↘ ↙ W \array{ W && \overset{\sigma}{\longrightarrow} && B \\ & {}_{\mathllap{id}}\searrow && \swarrow_{\mathrlap{}} \\ && W }
in 𝒞\mathcal{C}.
-
The interpretation of the dependent computation rules is that the section σ\sigma from above is required to be an algebra homomorphism.
Proposition
When interpreted in a category 𝒞\mathcal{C} of homotopy 0-types = sets, definition 1 and definition 2 are indeed equivalent.
Proof
First suppose that WW is an initial FF-algebra as in def. 2. Then since initiality entails first of all the existence of a morphims to any other object it follows that with BB another FF-algebra there is a homomorphism W→BW \to B, and since secondly initiality entails uniqueness of this morphism, it follows that given a homomorphism B→WB \to W the composite W→B→WW \to B \to W has to equal the identity id Wid_W, hence that B→WB \to W has a section, and uniquely so.
Conversely, assume that WW satisfies definition 1. For AA any other FF-algebra we can form the trivial display map W×A→WW \times A \to W by projection and a section of this is equivalently just a morphism W→AW \to A, so we have a homomorphism from WW to any other FF-algebra AA. Therefore to show that WW is an initial FF-algebra it remains to show that for f,g:W→Af, g : W \to A two algebra homomorphism, they are necessarily equal.
To that end, notice that by the assumption of 0-truncation, the diagonal δ:A→A×A\delta \colon A \to A \times A is a display map / fibration.
Form its pullback PP
P → A ↓ ↓ δ W →⟨f,g⟩ A×A,, \array{ P & \to & A \\ \downarrow & & \downarrow^\mathrlap{\delta} \\ W & \underset{\langle f, g \rangle}{\to} & A \times A, } \,,
which is also an algebra homomorphism. Therefore by the interpretation of the elimination rule it has a (specified) section σ:W→P\sigma : W \to P. But P→WP \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 ff and gg are equal.
Properties
Homotopy initiality
Any inductive type WW is a homotopy initial F-algebra: the space of FF-algebra maps W→XW \to X is contractible.
[[Awodey, Gambino & Sojakova (2012)](#AwodeyGambinoSojakova12)]
Examples
In the first examples to follow, the computation rules are written with ordinary equality signs “=”. At least for extensional inductive types these are judgemental equalities.
\linebreak
Empty type
The inductive inference rules for the empty type:
| |∅:Type \frac{ }{ \mathclap{\phantom{\vert^{\vert}}} \varnothing \,\colon\, Type }
\linebreak
--- none --- \text{--- none ---}
\linebreak
x:∅⊢D(x):Type| |ind (D):∏x:∅D(x) \frac{ x \,\colon\, \varnothing \;\vdash\;\; D(x) \,:\, Type }{ \mathclap{\phantom{\vert^{\vert}}} ind_{(D)} \,\colon\, \underset{x \colon \varnothing}{\prod} D(x) }
\linebreak
--- none --- \text{--- none ---}
Unit type
The inductive inference rules for the unit type:
| |*:Type \frac{ }{ \mathclap{\phantom{\vert^{\vert}}} \ast \,\colon\, Type }
\linebreak
| |pt:* \frac{ }{ \mathclap{\phantom{\vert^{\vert}}} pt \,\colon\, \ast }
\linebreak
x:*⊢D(x):Type;pt D:D(pt)| || |ind (D,pt D):∏x:*D(x) \frac{ x \,\colon\, \ast \;\vdash\;\; D(x) \,:\, Type \;; \;\;\; pt_D \,\colon\, D(pt) \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} ind_{(D,\,pt_D)} \,\colon\, \underset{x \colon \ast}{\prod} D(x) }
\linebreak
ind (D,pt D)(pt)=pt D ind_{(D,\,pt_D)}(pt) \;=\; pt_D
\linebreak
Booleans
The inference rules for the type of classical truth values/bits (the classical boolean domain):
\linebreak
Bit:Type \frac{ }{ Bit \,\colon\, Type }
\linebreak
0:Bit1:Bit \frac{ }{ 0 \,\colon\, Bit } \;\;\;\;\; \frac{ }{ 1 \,\colon\, Bit }
\linebreak
b:Bit⊢P(b);0 P:P(0);1 P:P(1)ind (P,0 P,1 P):∏b:BitP(b) \frac{ b \,\colon\, Bit \;\vdash\; P(b) ;\; \;\; 0_P \,\colon\, P(0) ;\; \;\; 1_P \,\colon\, P(1) }{ ind_{(P,\,0_P,\,1_P)} \,\colon\, \underset{b \colon Bit}{\prod} P(b) }
\linebreak
b:Bit⊢P(b);0 P:P(0);1 P:P(1)ind (P,0 P,1 P)(0)=0 P; ind (P,0 P,1 P)(1)=1 P \frac{ b \,\colon\, Bit \;\vdash\; P(b) ;\; \;\; 0_P \,\colon\, P(0) ;\; \;\; 1_P \,\colon\, P(1) }{ \begin{array}{l} ind_{(P,\,0_P,\,1_P)}(0) \;=\; 0_P ;\; \\ ind_{(P,\,0_P,\,1_P)}(1) \;=\; 1_P \end{array} }
See at Boolean domain – In type theory
\linebreak
Natural numbers
The inductive inference rules for the natural numbers type:
\linebreak
-
| |ℕ:Type \frac{}{ \mathclap{\phantom{\vert^{\vert}}} \mathbb{N} \,\colon\, Type }
-
| |0:ℕn:ℕ| || |succ(n):ℕ \frac{}{ \mathclap{\phantom{\vert^{\vert}}} 0 \,\colon\, \mathbb{N} } \;\;\;\;\;\;\;\; \frac{ n \,\colon\, \mathbb{N} \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} succ(n) \,\colon\, \mathbb{N} }
-
n:ℕ⊢P(n):Type;⊢0 P:P(0);n:ℕ,p:P( x n)⊢succ P(n,p):P(succ(n))| || |n:ℕ⊢ind (P,0 P,succ P)(n):P(n) \frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(n) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) P(n) \;\vdash\; succ_P(n,\,p) \,\colon\, P\big(succ(n)\big) \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} n \,\colon\, \mathbb{N} \;\vdash\; ind_{(P, 0_P, succ_P)}(n) \,\colon\, P(n) }
-
n:ℕ⊢P(n):Type;⊢0 P:P(0);n:ℕ,p:P( x n)⊢succ P(n,p):P(succ(n))| || |ind (P,0 P,succ P)(0)=0 P \frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(n) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) P(n) \;\vdash\; succ_P(n,p) \,\colon\, P\big(succ(n)\big) \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} ind_{(P, 0_P, succ_P)}(0) \,=\, 0_P }
and
n:ℕ⊢P(x):Type;⊢0 P:P(0);n:ℕ,p:P( x n)⊢succ P( x n,p):P(s x n);⊢n:ℕ| || |ind (P,0 P,succ P)(succ(n))=succ P(n,ind (P,0 P,succ P)(n)) \frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(x) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) P(n) \;\vdash\; succ_P(x,p) succ_P(n,p) \,\colon\, P(s x) n) \;; \;\;\;\; \vdash\; n \,\colon\, \mathbb{N} \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} ind_{(P, 0_P, succ_P)}\big(succ(n)\big) \,=\, succ_P\big(n,\, ind_{(P, 0_P, succ_P)}(n) \big) }
\linebreak
Lists
If XX is any set, then the inductive type LXL X of lists of elements of XX has |X|+1|X|+1 constructors:
- nilnil of arity zero, and
- cons(x,−)cons(x,-) of arity one, for each x∈Xx\in X.
Therefore, nilnil is a list, cons(x,ℓ)cons(x,\ell) is a list for any list ℓ\ell and x∈Xx\in X, and all lists are generated in this way.
Identity types
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.Categorical semantics
We may interpret identity types in suitable categories 𝒞\mathcal{C} such as a type-theoretic model category.
Example
The categorical interpretation of identity types in a category 𝒞\mathcal{C} is as the initial algebra for the endofunctor
F:𝒞 /A×A→𝒞 /A×A F : \mathcal{C}_{/A \times A} \to \mathcal{C}_{/A \times A}
of the slice category 𝒞 /A×A\mathcal{C}_{/A \times A} over A×AA\times A which is constant at the diagonal A→A×AA\to A\times A:
F(⟨E→A×A⟩)=⟨A→ΔA×A⟩. F (\langle E \to A \times A\rangle) = \langle A \stackrel{\Delta}{\to} A \times A\rangle \,.
So an algebra for this endofunctor is a morphism
A → E Δ↘ ↙ A×A \array{ A &&\to&& E \\ & {}_{\mathllap{\Delta}}\searrow && \swarrow \\ && A \times A }
and the initial such is the path space object A I→A×AA^I \to A \times A.
Path induction
Example
We spell out in detail how the the induction principle def. 1 for identity types is the principle of substitution of equals for equals.
To have an FF-algebra ⟨E→A×A⟩\langle E \to A\times A\rangle over ⟨A I→A×A⟩\langle A^I \to A \times A\rangle means precisely to have a diagram
E ↗ ↓ A → A I ↘ ↓ A×A \array{ && E \\ & \nearrow& \downarrow \\ A &\to& A^I \\ &\searrow& \downarrow \\ && A \times A }
in 𝒞\mathcal{C}.
This is the interpretation of the elimination rule: E→A IE \to A^I is the interpretation of a type
a,b∈A,p:(a=b)⊢E(a,b,p) a,b \in A , p : (a = b) \vdash E(a,b,p)
and the lift A→EA \to E is a section of the pullback of EE to AA, hence an interpretation of a term in the substitution
s:E(a,a,r a). s : E(a,a,r_a) \,.
The elimination rule then says that this extends to a section A I→EA^I \to E, hence a “proof of EE over all identifications” a=ba = b.
Path recursion
Example
We spell out how the the recursion principle def. 2 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 1,
X 0 →σ 0 X 1 ↘ ↙ δ 0,δ 1 X 0×X 0 \array{ X_0 &&\stackrel{\sigma_0}{\to}&& X_1 \\ & \searrow && \swarrow_{\mathrlap{\delta_0, \delta_1}} \\ && X_0 \times X_0 }
constitutes the 1-skeleton of a simplicial object
X 1 δ 0↓↑ σ 0↓ δ 1 X 0. \array{ X_1 \\ {}^{\mathllap{\delta_0}}\downarrow \uparrow^{\mathrlap{\sigma_0}} \downarrow^{\mathrlap{\delta_1}} \\ X_0 } \,.
The recursion principle says that the degeneracy map σ 0\sigma_0 factors through the path space object of X 0X_0 as a lift σ^ 0\hat \sigma_0 in the diagram
X 0 →σ 0 X 1 ↓ ↗ σ^ 0 ↓ X 0 I → X 0×X 0. \array{ X_0 &\stackrel{\sigma_0}{\to}& X_1 \\ \downarrow &\nearrow_{\hat \sigma_0}& \downarrow \\ X_0^I &\to& X_0 \times X_0 } \,.
Semantically, this lift exists because X 0→X 0 IX_0 \to X_0^I is an acyclic cofibration by definition of path space object, and X 1→X 0×X 0X_1 \to X_0 \times X_0 is a fibration (display map) by the interpretation rule for dependent types.
This morphism
σ^ 0:X 0 I→X 1 \hat \sigma_0 : X_0^I \to X_1
lifts paths/morphisms that exist in X 0X_0 to the morphisms exhibited by X 1X_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 1X_1, those morphisms that are invertible with respect to the given composition operation. In good situations this will give the core inclusion
Core(X 1)↪X 1. Core(X_1) \hookrightarrow X_1 \,.
In this case the Segal-completeness condition in degree 1 says that the path recursion σ^ 0\hat \sigma_0 exhibits this inclusion
σ^ 0:X 0 I≃Core(X 1)→X 1. \hat \sigma_0 : X_0^I \simeq Core(X_1) \to X_1 \,.
In the case that X •X_\bullet is the classifier of the codomain fibration, then this is called the univalence-condition.
W-types
References
Could not include history of inductive types – references
Introduction and review
Textbook accounts:
-
Simon Thompson, §4.10 in: Type Theory and Functional Programming, Addison-Wesley (1991) [ISBN:0-201-41667-0, webpage, pdf]
-
Adam Chlipala, §3 of: Certified programming with dependent types, MIT Press 2013 [[ISBN:9780262026659 ](https://mitpress.mit.edu/books/certified-programming-dependent-types), pdf, book webpage]
(discussion for the Coq proof assistant)
-
Robert Harper, §15 in: Practical Foundations for Programming Languages, Cambridge University Press (2016) [[ISBN:9781107150300](http://www.cambridge.org/us/academic/subjects/computer-science/programming-languages-and-applied-logic/practical-foundations-programming-languages-2nd-edition?format=HB), pdf]
See also:
- Wikipedia, Inductive types
Exposition with an eye towards explaining identity types in Martin-Löf type theory/homotopy type theory:
- Mike Shulman, Induction on equality (2011) [[pdf](http://home.sandiego.edu/~shulman/papers/induction.pdf), pdf]
Formalization in proof assistants:
in Coq:
- Eduardo Giménez, Pierre Castéran, A Tutorial on [Co-]Inductive Types in Coq (1998, 2005) [[pdf](http://flint.cs.yale.edu/cs428/coq/pdf/RecTutorial.pdf), pdf]
in Lean:
On inductive types in the context of linear type theory:
- Stéphane Gimenez, Towards Generic Inductive Constructions in Systems of Nets [[pdf](https://www.imn.htwk-leipzig.de/~waldmann/WST2013/papers/paper_16.pdf)]
Expositions with an eye towards higher inductive types:
-
Mike Shulman, Homotopy type theory IV (web)
-
Peter LeFanu Lumsdaine, Higher inductive types, a tour of the menagerie (blog post)
-
Mike Shulman, Inductive and higher inductive types, talk slides (2012) (pdf)
Discussion of homotopy-initiality of inductive types in homotopy type theory (cf. also at higher inductive type):
-
Steve Awodey, Nicola Gambino, Kristina Sojakova, Inductive types in homotopy type theory, LICS’12: (2012) 95–104 [[arXiv:1201.3898](http://arxiv.org/abs/1201.3898), doi:10.1109/LICS.2012.21, Coq code]
\linebreak
Exposition:
Steve Awodey, Inductive types in HoTT (Jan 2012) [[blog post](http://homotopytypetheory.org/2012/01/19/inductive-types-in-hott/)]
Categorical semantics of 𝒲\mathcal{W}-types
The observation that the categorical semantics of well-founded inductive types ($\mathcal{W}$-types) is given by initial algebras over polynomial endofunctors on the type system:
-
Peter Dybjer, Representing inductively defined sets by wellorderings in Martin-Löf’s type theory, Theoretical Computer Science 176 1–2 (1997) 329-335 [[doi:10.1016/S0304-3975(96)00145-4]]
-
Ieke Moerdijk, Erik Palmgren, Wellfounded trees in categories, Annals of Pure and Applied Logic 104 1-3 (2000) 189-218 [[doi:10.1016/S0168-0072(00)00012-9]]
Further discussion:
-
Michael Abbott, Thorsten Altenkirch, Neil Ghani, Containers: Constructing strictly positive types, Theoretical Computer Science 342 1 (2005) 3-27 [[doi:10.1016/j.tcs.2005.06.002]]
-
Benno van den Berg, Ieke Moerdijk, WW-types in sheaves [[arXiv:0810.2398](https://arxiv.org/abs/0810.2398)]
Generalization to inductive families (dependent 𝒲\mathcal{W}-types):
-
Nicola Gambino, Martin Hyland, Wellfounded Trees and Dependent Polynomial Functors, in: Types for Proofs and Programs TYPES 200, Lecture Notes in Computer Science 3085, Springer (2004) [[doi:10.1007/978-3-540-24849-1_14]]
-
Michael Abbott, Thorsten Altenkirch, Neil Ghani: Representing Nested Inductive Types using W-types, in: Automata, Languages and Programming, ICALP 2004, Lecture Notes in Computer Science, 3142, Springer (2004) [[doi:10.1007/978-3-540-27836-8_8, pdf]]
exposition: Inductive Types for Free – Representing nested inductive types using W-types, talk at ICALP (2004) [[pdf]]
Generalization to homotopy-initial algebras as categorical semantics for $\mathcal{W}$-types in homotopy type theory:
-
Steve Awodey, Nicola Gambino, Kristina Sojakova, Inductive types in homotopy type theory, LICS’12: (2012) 95–104 [[arXiv:1201.3898, doi:10.1109/LICS.2012.21, Coq code]]
-
Benno van den Berg, Ieke Moerdijk, W-types in Homotopy Type Theory, Mathematical Structures in Computer Science 25 Special Issue 5: From type theory and homotopy theory to Univalent Foundations of Mathematics (2015) 1100-1115 [[arXiv:1307.2765, doi:10.1017/S0960129514000516]]
-
Kristina Sojakova, Higher Inductive Types as Homotopy-Initial Algebras, ACM SIGPLAN Notices 50 1 (2015) 31–42 [[arXiv:1402.0761, doi:10.1145/2775051.2676983]]
-
Steve Awodey, Nicola Gambino, Kristina Sojakova, Homotopy-initial algebras in type theory, Journal of the ACM 63 6 (2017) 1–45 [[arXiv:1504.05531, doi:10.1145/3006383]]
-
Benno van den Berg, Ieke Moerdijk, W-types in Homotopy Type Theory, Mathematical Structures in Computer Science 25 Special Issue 5: From type theory and homotopy theory to Univalent Foundations of Mathematics (2015) 1100-1115 [[arXiv:1307.2765](http://arxiv.org/abs/1307.2765), doi:10.1017/S0960129514000516]
Towards combining generalization to dependent and homotopical W-types:
- Christian Sattler, On relating indexed W-types with ordinary ones, in Types for Proofs and Programs – TYPES 2015 (2015) 71-72 [[pdf, pdf]]
Last revised on February 24, 2024 at 15:19:47. See the history of this page for a list of all contributions to it.