[go: up one dir, main page]
More Web Proxy on the site http://driver.im/

nLab inductive type

Contents

Context

Deduction and Induction

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

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.

  1. term introduction rule

    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 \,.
  2. term elimination rule

    The interpretation of the dependent elimination rule says that given a display map BWB \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 σ:WB𝒞 /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}.

  3. computation rule

    The interpretation of the dependent computation rules is that the section σ\sigma from above is required to be an algebra homomorphism.

Definition

The categorical interpretation of recursion, hence of the absolute elimination rules from above in a suitable category 𝒞\mathcal{C} is the following

  1. term introduction rule

    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 \,.
  2. term elimination rule

    The interpretation of the absolute elimination rule is that for AA any other FF-algebra, there is a morphism WAW \to A in 𝒞\mathcal{C}.

  3. computation rule

    The interpretation of the absolute computation rule says that the morphism WAW \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.

Proposition

When interpreted in a category 𝒞\mathcal{C} of homotopy 0-types = sets, definition and definition are indeed equivalent.

Proof

First suppose that WW is an initial FF-algebra as in def. . 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 WBW \to B, and since secondly initiality entails uniqueness of this morphism, it follows that given a homomorphism BWB \to W the composite WBWW \to B \to W has to equal the identity id Wid_W, hence that BWB \to W has a section, and uniquely so.

Conversely, assume that WW satisfies definition . For AA any other FF-algebra we can form the trivial display map W×AWW \times A \to W by projection and a section of this is equivalently just a morphism WAW \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:WAf, g : W \to A two algebra homomorphism, they are necessarily equal.

To that end, notice that by the assumption of 0-truncation, the diagonal δ:AA×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 σ:WP\sigma : W \to P. But PWP \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.

Remark

In intensional type theory, where the diagonal is not a display map, we can perform the same argument using a path object PAA×AP A \to A \times A (represented in type theory by an identity type), showing thereby that ff and gg are homotopic. A fancier version of this argument enables us to show that the space of algebra maps WAW\to A is actually contractible. In other words, the axioms for an inductive type still imply that algebra maps out of WW are essentially unique, even though the axioms do not state this explicitly.

Properties

Homotopy initiality

Any inductive type WW is a homotopy initial F-algebra: the space of FF-algebra maps WXW \to X is contractible.

[Awodey, Gambino & Sojakova (2012)]

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.


Empty type

The inductive inference rules for the empty type:

type formation rule:

| |:Type \frac{ }{ \mathclap{\phantom{\vert^{\vert}}} \varnothing \,\colon\, Type }


term introduction rule:

--- none --- \text{--- none ---}


term elimination rule:

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) }


computation rule:

--- none --- \text{--- none ---}

Unit type

The inductive inference rules for the unit type:

type formation rule:

| |*:Type \frac{ }{ \mathclap{\phantom{\vert^{\vert}}} \ast \,\colon\, Type }


term introduction rule:

| |pt:* \frac{ }{ \mathclap{\phantom{\vert^{\vert}}} pt \,\colon\, \ast }


term elimination rule:

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) }


computation rule:

ind (D,pt D)(pt)=pt D ind_{(D,\,pt_D)}(pt) \;=\; pt_D


Booleans

The inference rules for the type of classical truth values/bits (the classical boolean domain):


type formation rule:

Bit:Type \frac{ }{ Bit \,\colon\, Type }


term introduction rule:

0:Bit1:Bit \frac{ }{ 0 \,\colon\, Bit } \;\;\;\;\; \frac{ }{ 1 \,\colon\, Bit }


term elimination rule:

b:BitP(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) }


computation rules:

b:BitP(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


Natural numbers

The inductive inference rules for the natural numbers type:


  1. type formation rule:

    | |:Type \frac{}{ \mathclap{\phantom{\vert^{\vert}}} \mathbb{N} \,\colon\, Type }
  2. term introduction rules:

    | |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} }
  3. term elimination rule:

    n:P(n):Type;0 P:P(0);n:,p:P(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(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) }
  4. computation rules:

    n:P(n):Type;0 P:P(0);n:,p:P(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(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(n)succ P(n,p):P(sn);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(n) \;\vdash\; succ_P(n,p) \,\colon\, P(s 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) }


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 xXx\in X.

Therefore, nilnil is a list, cons(x,)cons(x,\ell) is a list for any list \ell and xXx\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 AA×AA\to A\times A:

F(EA×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 IA×AA^I \to A \times A.

Path induction

Example

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 FF-algebra EA×A\langle E \to A\times A\rangle over A IA×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: EA IE \to A^I is the interpretation of a type

a,bA,p:(a=b)E(a,b,p) a,b \in A , p : (a = b) \vdash E(a,b,p)

and the lift AEA \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 IEA^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. 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 ,

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 0X 0 IX_0 \to X_0^I is an acyclic cofibration by definition of path space object, and X 1X 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 IX 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 ICore(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

History of inductive types

Historical references on the definition of inductive types.

Precursors

A first type theoretic formulation of general inductive definitions:

The induction principle for identity types (also known as “path induction” or the “J-rule”) is first stated in:

  • Per Martin-Löf, §1.7 and p. 94 of: An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 (1975) 73-118 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)

and in the modern form of inference rules in:

  • Bengt Nordström, Kent Petersson, Jan M. Smith, §8.1 of: Programming in Martin-Löf’s Type Theory, Oxford University Press (1990) [[webpage, pdf, pdf]]

The special case of inductive types now known as 𝒲 \mathcal{W} -types is first formulated in:

Early proposals for a general formal definition of inductive types:

Modern definition

The modern notion of inductive types and inductive families in intensional type theory is independently due to

and due to

which became the basis of the calculus of inductive constructions used in the Coq-proof assistant:

reviewed in

with streamlined exposition in:

The generalization to inductive-recursive types is due to

See also:

Introduction and review

Textbook accounts:

See also:

Exposition with an eye towards explaining identity types in Martin-Löf type theory/homotopy type theory:

Formalization in proof assistants:

in Coq:

  • Eduardo Giménez, Pierre Castéran, A Tutorial on [Co-]Inductive Types in Coq (1998, 2005) [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]

Expositions with an eye towards higher inductive types:

Discussion of homotopy-initiality of inductive types in homotopy type theory (cf. also at higher inductive type):

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:

Further discussion:

Generalization to inductive families (dependent 𝒲\mathcal{W}-types):

Generalization to homotopy-initial algebras as categorical semantics for 𝒲 \mathcal{W} -types in homotopy type theory:

Towards combining generalization to dependent and homotopical W-types:

Last revised on February 24, 2024 at 15:19:47. See the history of this page for a list of all contributions to it.