Inductive Types in HoTT

With all the excitement about higher inductive types (e.g. here and here), it seems worthwhile to work out the theory of conventional (lower?) inductive types in HoTT. That’s what Nicola Gambino, Kristina Sojakova and I have done, as we report in the following paper that’s just been posted on the archive:

Inductive types in Homotopy Type Theory, S. Awodey, N. Gambino, K. Sojakova, January 2012, arXiv:1201.3898v1.

The main theorem is that in HoTT, what we call the rules for homotopy W-types are equivalent to the existence of homotopy-initial algebras for polynomial functors. The required definitions are as follows:

the rules for homotopy W-types: the usual rules for W-types of formation, introduction, (dependent) elimination, and computation — but the latter is formulated as a propositional rather than a definitional equality.
a weak map of algebras $(A, s_A) \to (B, s_B)$ is a map $f:A\to B$ together with an identity proof $f\circ s_A \sim s_B\circ Pf$ , where $P$ is the polynomial functor, and a $P$ -algebra is just a map $s_A : PA\to A$ , as usual.
an algebra $(C, s_C)$ is homotopy-initial if for every algebra $(A, s_A)$ , the type of all weak maps $(C, s_C) \to (A, s_A)$ is contractible.

So in brief, the extensional situation where “W-type = initial $P$ -algebra” now becomes “homotopy W-type = homotopy-initial $P$ -algebra”. Perhaps not very surprising, once one finds the right concepts; but satisfying nonetheless.

We focus mainly on W-types because most conventional inductive types like $\mathsf{Nat}$ can be reduced to these; in fact, the possibility of such reductions is itself part of our investigation. There are some results in extensional type theory (cited in the paper) showing that many inductive types are reducible to W-types, and there is some literature (also cited) showing how such reductions can fail in the purely intensional theory. We show that in HoTT some of these reductions go through, provided both the W-types and the inductive types are understood in the appropriate “homotopical” way, with propositional computation rules. The detailed investigation of more such reductions is left as future work.

Of course, the entire development has been formalized in Coq. The files are available in the HoTT repo on GitHub:

https://github.com/HoTT/HoTT/tree/master/Coq/IT

There are also some slides (and even a video somewhere) from a talk I recently gave about this at the MAP Workshop, at the Lorentz Center in Leiden. These can be found here.

This entry was posted in Code, Foundations, Paper. Bookmark the permalink.

9 Responses to Inductive Types in HoTT

Mike Shulman says:

21 January 2012 at 03:47

This is very nice! Have you thought at all about coinductive types?

Reply
- Martin Escardo says:
  
  22 February 2012 at 06:58
  
  As a modest result in that direction, I show how to construct the final co-algebra of 1+(-) and prove finality using extensionality: http://www.cs.bham.ac.uk/~mhe/agda/CoNaturals.html
  
  But I also wonder what co-inductive types can be defined in type theory.
  
  Reply
  - Steve Awodey says:
    
    22 February 2012 at 10:29
    
    I believe that Agda imposes Uniqueness of Identity proofs (UIP), which makes this development less than fully general. That said, the overall form of the argument seems likely to be doable in general HoTT, so wouldn’t doubt that that same will hold there. It’s a very nice start anyway.
    
    Reply
    - Martin Escardo says:
      
      22 February 2012 at 10:32
      
      Agda has the option without-K, which I am using. I am also taking explicit care of not using UIP in all my agda files, except in cases where it can be proved (from extensionality).
      
      Reply
  - Mike Shulman says:
    
    13 March 2012 at 22:58
    
    Finally had a chance to look at this. It is nice, but it’s not what I was thinking of; what I had in mind was actual coinductive definitions along the lines of Coq’s CoInductive or Agda’s codata. Am I missing something?
    
    Reply
    - Martin Escardo says:
      
      14 March 2012 at 05:39
      
      I am not sure what you have in mind. Co-induction/recursion is about final co-algebras. The rest is syntax sugar, isn’t it? And perhaps we don’t have optimal syntax sugar in Agda or Coq, do we? (And codata has been removed from Agda in favour of “sharp” and “flat” in the style of delay and force in Scheme, within “data” definitions.) The paper advertised by Steve likewise focuses on initial algebras, rather than on syntax for induction and recursion. In the Agda file mentioned above, there is a co-recursion combinator (X -> 1+X) -> X -> CoN and a co-induction principle for CoN using bisimulations in the standard way.
      
      It would be interesting to answer the question whether all the co-inductive types definable in Agda and Coq are or are not already definable in ML type theory (assuming extensionality, as done by Steve et al). For example, streams and non-well founded trees are already definable. This covers quite a lot. Also, the so-called delay monad is definable (generalizing the idea used to define CoN). Can you come up with a co-inductive type that is not definable in ML type theory? I think this is an interesting question (which you asked above!).
      
      Reply
      - Mike Shulman says:
        
        16 March 2012 at 01:22
        
        I sort of agree. Yes, coinduction is morally about final coalgebras, in the same way that induction is morally about initial algebras. But the way that we formulate that in type theory isn’t necessarily just syntactic sugar; it can affect how they behave.
        
        For instance, the usual formulation of inductive types specifies that any algebra-fibration over the inductive type has an algebra-section. It’s not immediately obvious that this is the same as being an initial algebra, which is why Steve, Nicola, and Kristina’s paper is interesting and important. And they only proved the equivalence of homotopy-initial-algebras with W-types having a propositional computation rule, so the usual formulation of inductive types is stronger than merely being a homotopy initial algebra. Maybe not much stronger, but stronger in a very useful way!
        
        That said, I certainly agree that there is nothing sacred about the particular choices made regarding the behavior of coinductive types in Coq/Agda. In particular, I find it odd that one can match on a coinductive type with a definitional computation rule. Homotopically, matching on an inductive type corresponds roughly to saying that the algebra map $F(W)\to W$ is an acyclic cofibration, so by duality it seems that a coinductive type should have the property that $M\to F(M)$ is an acyclic fibration, not that its inverse $F(M) \to M$ is an acyclic cofibration.
        
        I guess what I would really like to see answered is the same thing that you ask: can all coinductive definitions be translated in such a way using inductive ones and function extensionality? Now that I think some more about your construction, it does seem plausible.
        
        Reply
        
        Martin Escardo says:
        
        16 March 2012 at 05:36
        
        Good! We seem to agree. In particular, it is very true, as you say, that good syntax allows us to think in a better way (just as in classical mathematics, in e.g. algebra). But my modest goal was to merely exhibit an example of a coinductive type that exists in MLTT+Ext, in addition to the folklore example of streams, and not to contribute to the discussion of what a good syntax for coinduction should (not) be.
        
        I also find the matching you mention very odd! But I don’t fully appreciate the argument you give above. Can you elaborate on that?
        
        Reply
        
        Mike Shulman says:
        
        19 March 2012 at 18:13
        
        Coq’s basic match syntax for inductive types, specialized to the natural numbers, says that if we have a dependent type over the naturals, i.e. a display map a.k.a. fibration $P \to N$ , and a section of the pullback of $P$ along $(0,s)\colon 1+N\to N$ , then we have a section of $P$ over $N$ . If you write that out as a lifting property, it means that $(0,s)$ has the left lifting property with respect to fibrations, i.e. it is an acyclic cofibration. Of course, $(0,s)$ is the structure map making $N$ into an algebra for $F(X) = 1+X$ . When you add recursive matches / fixpoints too, then $(0,s)$ has some additional initial-algebra-ish property.
        
        Now if you turn all the arrows around, I would expect some sort of “comatch” operation that would make the structure map $M \to F(M)$ of a coinductive type into an acyclic fibration. Unfortunately, it’s a bit difficult to formulate a right lifting property in type theory, since we don’t have a way to say inside of type theory “let $i$ be a cofibration” in the same way that we can say “let $p$ be a fibration” (namely, by saying “let $P$ be a dependent type”). But we do know that the acyclic fibrations are the fibrations with contractible fibers; maybe that could be expressed in the coinductive rules somehow.
        
        Reply