5.5 Homotopy-inductive types

In Β§5.3 (http://planetmath.org/53wtypes) we showed how to encode natural numbersMathworldPlanetmath as 𝖢-types, with

𝐍𝐰 :≑𝖢(b:𝟐)π—‹π–Ύπ–ΌπŸ(𝒰,𝟎,𝟏),
0𝐰 :β‰‘π—Œπ—Žπ—‰(0𝟐,(Ξ»x.π—‹π–Ύπ–ΌπŸŽ(𝐍𝐰,x))),
𝐬𝐰 :≑λn.π—Œπ—Žπ—‰(1𝟐,(Ξ»x.n)).

We also showed how one can define a π–½π—ˆπ—Žπ–»π—…π–Ύ function on 𝐍𝐰 using the recursion principle. When it comes to the inductionMathworldPlanetmath principle, however, this encoding is no longer satisfactory: given E:𝐍𝐰→𝒰 and recurrences ez:E⁒(0𝐰) and es:∏(n:𝐍𝐰)∏(y:E(n))E⁒(𝐬𝐰⁒(n)), we can only construct a dependent function r⁒(E,ez,es):∏(n:𝐍𝐰)E⁒(n) satisfying the given recurrences propositionally, i.e.Β up to a path. This means that the computation rules for natural numbers, which give judgmental equalities, cannot be derived from the rules for 𝖢-types in any obvious way.

This problem goes away if instead of the conventional inductive types we consider homotopy-inductive types, where all computation rules are stated up to a path, i.e.Β the symbol ≑ is replaced by =. For instance, the computation rule for the homotopy version of 𝖢-types 𝖢𝗁 becomes:

  • β€’

    For any a:A and f:B⁒(a)→𝖢(x:A)h⁒B⁒(x) we have


Homotopy-inductive types have an obvious disadvantage when it comes to computational properties β€” the behavior of any function constructed using the induction principle can now only be characterized propositionally. But numerous other considerations drive us to consider homotopy-inductive types as well. For instance, while we showed in Β§5.4 (http://planetmath.org/54inductivetypesareinitialalgebras) that inductive types are homotopy-initial algebrasMathworldPlanetmathPlanetmath, not every homotopy-initial algebra is an inductive type (i.e.Β satisfies the corresponding induction principle) β€” but every homotopy-initial algebra is a homotopy-inductive type. Similarly, we might want to apply the uniqueness argument from Β§5.2 (http://planetmath.org/52uniquenessofinductivetypes) when one (or both) of the types involved is only a homotopy-inductive type β€” for instance, to show that the 𝖢-type encoding of β„• is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to the usual β„•.

Additionally, the notion of a homotopy-inductive type is now internal to the type theoryPlanetmathPlanetmath. For example, this means we can form a type of all natural numbers objects and make assertions about it. In the case of 𝖢-types, we can characterize a homotopy 𝖢-type 𝖢(x:A)⁒B⁒(x) as any type endowed with a supremumMathworldPlanetmathPlanetmath function and an induction principle satisfying the appropriate (propositional) computation rule:


In http://planetmath.org/node/87579Chapter 6 we will see some other reasons why propositional computation rules are worth considering.

In this sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, we will state some basic facts about homotopy-inductive types. We omit most of the proofs, which are somewhat technical.

Theorem 5.5.1.

For any A:U and B:Aβ†’U, the type Wd⁒(A,B) is a mere proposition.

It turns out that there is an equivalent characterization of 𝖢-types using a recursion principle, plus certain uniqueness and coherence laws. First we give the recursion principle:

  • β€’

    When constructing a function from the 𝖢-type 𝖢(x:A)h⁒B⁒(x) into the type C, it suffices to give its value for π—Œπ—Žπ—‰β’(a,f), assuming we are given the values of all f⁒(b) with b:B⁒(a). In other words, it suffices to construct a function


The associated computation rule for 𝗋𝖾𝖼𝖢(x:A)h⁒B⁒(x)⁒(C,c):(𝖢(x:A)⁒B⁒(x))β†’C is as follows:

  • β€’

    For any a:A and f:B⁒(a)→𝖢(x:A)h⁒B⁒(x) we have a witness β⁒(C,c,a,f) for equality


Furthermore, we assert the following uniqueness principle, saying that any two functions defined by the same recurrence are equal:

  • β€’

    Let C:𝒰 and c:∏(a:A)(B(a)β†’C)β†’C be given. Let g,h:(𝖢(x:A)h⁒B⁒(x))β†’C be two functions which satisfy the recurrence c up to propositional equality, i.e., such that we have

    Ξ²g :∏a,fg(π—Œπ—Žπ—‰(a,f))=c(a,Ξ»b.g(f(b))),
    Ξ²h :∏a,fh(π—Œπ—Žπ—‰(a,f))=c(a,Ξ»b.h(f(b))).

    Then g and h are equal, i.e. there is α⁒(C,c,f,g,βg,βh) of type g=h.

Recall that when we have an induction principle rather than only a recursion principle, this propositional uniqueness principle is derivablePlanetmathPlanetmath (Theorem 5.3.1 (http://planetmath.org/53wtypes#Thmprethm1)). But with only recursion, the uniqueness principle is no longer derivable β€” and in fact, the statement is not even true (exercise). Hence, we postulateMathworldPlanetmath it as an axiom. We also postulate the following coherence law, which tells us how the proof of uniqueness behaves on canonical elements:

  • β€’

    For any a:A and f:B⁒(a)β†’C, the following diagram commutes propositionally:



    where α abbreviates the path α⁒(C,c,f,g,βg,βh):g=h.

Putting all of this data together yields another characterization of 𝖢(x:A)⁒B⁒(x), as a type with a supremum function, satisfying simple elimination, computation, uniqueness, and coherence rules:

Theorem 5.5.2.

For any A:U and B:Aβ†’U, the type Ws⁒(A,B) is a mere proposition.

Finally, we have a third, very concise characterization of 𝖢(x:A)⁒B⁒(x) as an h-initial 𝖢-algebra:

Theorem 5.5.3.

For any A:U and B:Aβ†’U, the type Wh⁒(A,B) is a mere proposition.

It turns out all three characterizations of 𝖢-types are in fact equivalent:

Lemma 5.5.4.

For any A:U and B:A→U, we have


Indeed, we have the following theorem, which is an improvement over Theorem 5.4.7 (http://planetmath.org/54inductivetypesareinitialalgebras#Thmprethm3):

Theorem 5.5.5.

The types satisfying the formation, introduction, elimination, and propositional computation rules for W-types are precisely the homotopy-initial W-algebras.

Sketch of proof.

Inspecting the proof of Theorem 5.4.7 (http://planetmath.org/54inductivetypesareinitialalgebras#Thmprethm3), we see that only the propositional computation rule was required to establish the h-initiality of 𝖢(x:A)⁒B⁒(x). For the converse implication, let us assume that the polynomial functor associated to A:𝒰 and B:A→𝒰, has an h-initial algebra (W,sW); we show that W satisfies the propositional rules of 𝖢-types. The 𝖢-introduction rule is simple; namely, for a:A and t:B⁒(a)β†’W, we define π—Œπ—Žπ—‰β’(a,t):W to be the result of applying the structure mapPlanetmathPlanetmathPlanetmath sW:P⁒Wβ†’W to (a,t):P⁒W. For the 𝖢-elimination rule, let us assume its premisses and in particular that Cβ€²:W→𝒰. Using the other premisses, one shows that the type C:β‰‘βˆ‘(w:W)Cβ€²(w) can be equipped with a structure map sC:P⁒Cβ†’C. By the h-initiality of W, we obtain an algebra homomorphism (f,sf):(W,sW)β†’(C,sC). Furthermore, the first projectionPlanetmathPlanetmath 𝗉𝗋1:Cβ†’W can be equipped with the structureMathworldPlanetmath of a homomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, so that we obtain a diagram of the form



But the identity function 1W:Wβ†’W has a canonical structure of an algebra homomorphism and so, by the contractibility of the type of homomorphisms from (W,sW) to itself, there must be an identityPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath proof between the composite of (f,sf) with (𝗉𝗋1,s𝗉𝗋1) and (1W,s1W). This implies, in particular, that there is an identity proof p:𝗉𝗋1∘f=1W.

Since (𝗉𝗋2∘f)⁒w:C⁒((𝗉𝗋1∘f)⁒w), we can define


where the transport p* is with respect to the family


The verification of the propositional 𝖢-computation rule is a calculation, involving the naturality properties of operationsMathworldPlanetmath of the form p*. ∎

Finally, as desired, we can encode homotopy-natural-numbers as homotopy-𝖢-types:

Theorem 5.5.6.

The rules for natural numbers with propositional computation rules can be derived from the rules for W-types with propositional computation rules.

Title 5.5 Homotopy-inductive types