Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

April 24, 2011

Homotopy Type Theory, VI

Posted by Mike Shulman

This will be the last post in this introductory sequence, although I will probably continue to post about new developments in homotopy type theory from time to time. (If you’re interested in the subject, you should also follow the HoTT blog.) Today I want to talk about a new, somewhat more radical idea, which we are currently calling higher inductive types.

The version of this I’m going to present below arose at Oberwolfach in discussions between Peter Lumsdaine, Andrej Bauer, Michael Warren, and myself, and since then Chris Kapulkin has also joined us in thinking about them. Peter did the initial implementation in Coq and noticed many of the applications below; a couple are my own inventions. (He also simultaneously wrote a post for the HoTT blog on the same subject.) I’m also told that Dan Licata and Steve Awodey have independently been working on related ideas. We all believe that this idea has the potential to solve many of the problems of homotopy type theory in a clean way, and one which moreover accords well with both type-theoretic and homotopy-theoretic intuition.

First, though, I should say a bit about ordinary inductive types. Categorically, an inductive type is a (perhaps weakly) initial algebra for an endofunctor. Intuitively, this means that it is freely generated by some collection of operations (possibly nullary, or parametrized by other types).

For instance, the natural numbers are freely generated by one point (zero) and one endomorphism (successor). Categorically, they are the initial algebra for the endofunctor X1+XX\mapsto 1+X, for which an arbitrary algebra is a type XX with a map 1+XX1+X\to X, i.e. a point 1X1\to X and an endomorphism XXX\to X.

I’ve so far avoided using “programmer’s syntax” in this sequence of posts, but with inductive types it becomes too cumbersome to do so, and it’s good to get some familiarity with how the code looks anyway. In Coq syntax, therefore, we can define the natural numbers as

Inductive nat : Type :=
| zero : nat
| succ : nat -> nat.

In Agda, we would write this as

data nat : Set where
  zero : nat
  succ : nat -> nat

We say that nat has two constructors zero and succ, one of which takes no arguments and the other of which takes one argument of type nat. The “inductiveness” of the definition comes from the fact that succ takes an argument which is of the same type being defined. The universal property of nat says that to define a function from nat to XX, we just need to specify a point xXx\in X and an endomorphism f:XXf\colon X \to X. In Coq we would write the function g:Xg\colon \mathbb{N} \to X defined in this way as

Fixpoint g (n : nat) : X :=
  match n with
  | zero => x
  | succ n' => f (g n')
  end.

while in Agda we would write it as

g : nat -> X
g zero = x
g (succ n') = f (g n')

In other words, if nn is zero, then g(n)=xg(n)=x, whereas if nn is the successor of nn', then g(n)=f(g(n))g(n) = f(g(n')).

The ability to define functions out of an inductive type like this is sometimes called its elimination rule. The fact that the value of gg at a given natural number can be computed using the data xx and ff which were used to define it is then called the computation rule. (There’s also a fancier version of the elimination rule, with a corresponding computation rule, in which the target type XX is allowed to be dependent on the inductive type such as nat.)

An important thing to note is that in the presence of a universe, say “TypeType”, we can also define functions natTypenat\to Type by recursion, and such functions are the same as types dependent on natnat. Defining a dependent type by recursion is generally called “large elimination,” since TypeType is a “large object”.

Not all inductive types are “nontrivially recursive,” in the sense that the constructors take inputs of the type being defined. For instance, for any types AA and BB, their coproduct can be defined as an inductive type:

Inductive coprod (A B : Type) : Type :=
| inl : A -> coprod A B
| inr : B -> coprod A B.

(From now on I’ll give only the Coq syntax.) Here there are two constructors, one which takes an argument of type AA and one which takes an argument of type BB; neither takes an element of the type being defined. In categorical terms, this means that we have an initial algebra for a constant endofunctor XA+BX\mapsto A+B, which is of course just A+BA+B.

(In particular, note that identifying inductive types with algebras for endofunctors requires us to already know that the category in question has well-behaved coproducts. If we want to categorically construct coproducts as particular inductive types, as above, then we would need something more complicated, like joint-algebras for finite families of endofunctors. But if we work just in the type theory, then the elimination and computation rules for inductive types allow us to prove that coprod A B is, in fact, a coproduct of AA and BB, and moreover that these coproducts are disjoint and stable under pullback. I mentioned this fact last time; see this comment thread.)

Identity types, or path types, are also a special kind of inductive type (or, more precisely, of inductive family). Their definition is

Inductive paths (A : Type) : A -> A -> Type :=
| idpath : forall (a : A), paths A a a.

This says that for each aAa\in A, there is exactly one constructor of Paths A(a,a)Paths_A(a,a), namely the identity path, and no other constructors. And the “elimination rule” for identity paths that I’ve mentioned before is exactly the elimination rule for this inductive family.

Now it may seem like there’s something a bit funny going on; how can there be nontrivial paths when we inductively require there to only be one of them? See this post and this one for a bit of insight into that question. It turns out that some kinds of inductive families, like path types, can “automatically” introduce nontrivial homotopy theory, whereas others, like natural numbers and coproducts, can’t. (In the latter case, one can actually prove that they can’t. For instance, \mathbb{N} defined as above is provably a set (i.e. a 0-type), and coproduct coprojections are provably injective and disjoint. Such proofs generally do require large eliminations, however.)


The basic idea of higher inductive types is to allow ourselves to explicitly introduce nontrivial homotopy theory in an inductive type, rather than “implicitly” as with identity types. Specifically, in the definition of inductive types and families, we allow also constructors which produce elements of (iterated) path types of the inductive type being defined, rather than elements of the type itself. For instance, here is a higher-inductive definition of S 1S^1.

Inductive circle : Type :=
| base : circle
| loop : paths base base.

That is, a circle is inductively generated by a point base, and a path loop from base to itself. Its “elimination rule” says that to define a map circleXcircle \to X, for any type XX, it suffices to give a point xXx\in X and a path from xx to itself. (As before, there’s also a fancier version where XX can be a type dependent on circle.)

More generally, it is easy to see how to build any finite CW complex as a higher inductive type. Here is a 2-sphere:

Inductive sphere : Type :=
| base2 : sphere
| loop2 : paths (idpath base) (idpath base)

Here is a torus:

Inductive torus : Type :=
| base : torus
| meridian : paths base base
| equator : paths base base
| surf : paths (meridian @ equator) (equator @ meridian)

(I’m using @ to denote concatenation of paths, as in Andrej Bauer’s Coq files.) I think the ability to define these things is really important. Note that in all of our discussion so far, we’ve talked about doing homotopy theory, but we haven’t said anything about how to obtain the specific homotopy types we want to do homotopy with! Higher inductive types give us a straightforward and easy-to-work-with way to define such things.

But despite our suggestive naming, it seems that higher inductive types do not require the semantics to be nontrivially homotopical. For extensional semantics in a 1-category, no path-type admits any nontrivial loops, and so the “circle” is actually no different from a point. In fact, there is a converse too: by the universal property of the circle, if CircleCircle is contractible, then we can show that any two parallel paths, in any type, are equal (i.e. the type theory satisfies “UIP” or “axiom K”). So nontriviality of the circle encapsulates the nontriviality of the entire homotopy theory.

Therefore, univalence remains the only axiom we have (apart from the still-somewhat-nebulous quotient types) which guarantees the nontriviality of the homotopy theory of types. But is univalence alone sufficient to guarantee that all higher inductive types behave like the spaces we expect them to? A complete answer to this question would (it seems) require constructing a model which validates a general formulation of higher inductive types, which is still a question for the future, but we can obtain evidence for it by showing that specific higher inductive types behave in expected ways.

As one step in this direction, I was recently able to show (and formalized in Coq) that assuming the univalence axiom, we have Ω(S 1)\Omega(S^1)\cong \mathbb{Z}, where S 1S^1 is the circle type defined inductively as above. Since \mathbb{Z} is a set, it is its own π 0\pi_0, so this also implies π 1(S 1)\pi_1(S^1)\cong \mathbb{Z}. (This might be the first actual computation of a nontrivial homotopy group in homotopy type theory; I am not sure.) I also have confidence that homotopy type theory admits enough homotopical machinery, such as fibration sequences, to allow us to compute more familiar homotopy groups.


Here is another higher inductive type, perhaps even simpler than the circle:

Inductive interval : Type :=
| zero : interval
| one : interval
| segment : paths zero one.

That is, an interval is inductively generated by two points, zero and one, and a path between them. Its (non-dependent) elimination rule says that to define a map intervalXinterval \to X, for any type XX, it suffices to give two points x,yXx,y\in X and a path pPaths X(x,y)p\in Paths_X(x,y).

Of course, in homotopy theory an interval is contractible, and we can also prove this in homotopy type theory about the interval thusly defined. So you might think the interval type doesn’t buy us very much. But actually it does, because it makes homotopies “representable”; in homotopy-theoretic language, it is (unsurprisingly) an interval object. One consequence of this, which occurred to me in the midst of this discussion, is that as long as the computation rules for the interval are “definitional” (i.e. holds on the point-set level in the category of types, rather than only up to homotopy), we can prove function extensionality; see this post.

This suggests a way to think about higher inductive types in general: they supply the “left side” of homotopy theory which has so far been missing. The “right side” of homotopy theory, having to do with fibrations, is well-modeled in homotopy type theory: we have a weak factorization system analogous to (acyclic cofibrations, fibrations), we have a good notion of fibrations (= display map = dependent type) which is preserved by pullback, all objects are fibrant, and we have path objects. However, we have said nothing about a notion of cofibration, cofibrant objects, cell complexes, cylinder objects, or a (cofibration, acyclic fibration) factorization system. Higher inductive types supply all of these deficiencies.

For instance, in addition to CW complexes like spheres and tori, we can also build “parametrized cell complexes” by using constructors that take other types as inputs. Here is a cylinder type:

Inductive cylinder (A : Type) : Type :=
| inl : A -> cylinder A
| inr : A -> cylinder A
| seg : forall (a : A), paths (inl a) (inr a)

While the cylinder type will be equivalent to AA, just like the interval type was contractible, it has the homotopy-theoretic property of a cylinder object: maps out of it represent homotopies between functions ABA\to B, just like maps into the path object Σ a,bAPaths(a,b)\Sigma_{a,b\in A} Paths(a,b) represent homotopies between functions BAB\to A.

Similarly, here is the homotopy pushout of two functions f:ABf\colon A\to B and g:ACg\colon A \to C:

Inductive hpushout {A B C : Type} (f : A -> B) (g : A -> C) : Type :=
| inl : B -> hpushout f g
| inr : C -> hpushout f g
| glue : forall (a : A), paths (inl (f a)) (inr (g a)).

That is, the pushout of ff and gg is inductively generated by a map from BB, a map from CC, and a path between the images of f(a)f(a) and of g(a)g(a) for any aAa\in A. Similarly, we can expect to be able to construct any particular kind of finite homotopy colimit.

Lastly in this vein, we can construct mapping cylinders, as essentially a special case of the homotopy pushout:

Inductive mcyl {A B : Type} (f : A -> B) : Type :=
| inl : A -> mcyl f
| inr : B -> mcyl f
| mseg : forall (a : A), paths (inl a) (inr (f a)).

Of course, as usual the mapping cylinder will be homotopy equivalent to BB, but again it has a homotopy-theory value: it gives us the other weak factorization system, by the following argument.

Recall that identity types (or, more generally, inductive families) give us (according to Gambino and Garner) one WFS on the category of types, in which the right class of maps is (generated by) the projections from dependent types, which we call “display maps”. This WFS is like the (acyclic cofibration, fibration) factorization system in a model structure. A generating class of acyclic cofibrations is the singleton constructors: the constructors of inductive types that have only one constructor. To see this, consider a square

A f C g h B k D \array{A & \overset{f}{\to} & C \\ ^g\downarrow & & \downarrow^h \\ B & \underset{k}{\to} & D}

in which gg is a singleton constructor and hh a display map. We must define a map n:BCn\colon B\to C such that hn=kh n = k and ng=fn g = f. But since CC is an inductive type and gg its only constructor, to define a map n:BCn\colon B \to C it suffices to give its composition with gg, namely ff; then we will have ng=fn g = f by definition, and hn=kh n = k will follow from hf=kgh f = k g.

Now we also have a natural class of weak equivalences, namely the homotopy equivalences, and we can characterize the acyclic fibrations: a display map BAB\to A is an equivalence iff each type B(x)B(x) is contractible (in a way continuously parametrized by AA, i.e. Π xAIsContr(B(x))\Pi_{x\in A} IsContr(B(x))). If we suppose that hh, above, has this property, then what additional maps gg satisfy the lifting property with respect to it?

It turns out that the answer is arbitrary constructors of (possibly higher) inductive types. For if gg is any constructor of an inductive type, to define n:BCn\colon B\to C it suffices to define its value constructor-by-constructor. On the particular constructor gg we can do as before, while for any other constructor we can use the continuous contractibility of the fibers of hh to select a point in the necessary fiber, making the lower triangle commute. (The value of nn on constructors other than gg has no effect on commutativity of the upper triangle.)

Now that argument looks as though it only requires the fibers of hh to be (continuously) inhabited, i.e. for hh to be split epic. And, indeed, we should have a WFS looking something like (constructors of inductive types, split-epic display maps). However, we need hh to be an acyclic fibration if we want it to also have the lifting property with respect to constructors of higher inductive types. For in that case, there may be paths in BB which connect points arising from different constructors, and to define nn on these paths, we need to use contractibility of the fibers of hh.

Thus, it makes sense to take as (generating) cofibrations the class of constructors of (higher) inductive types. All that’s missing to obtain a WFS in this way, therefore, is a factorization of an arbitrary map into a cofibration followed by an acyclic fibration. The mapping cylinder will give us this, if we modify it a bit so that it gives an output which is dependent on the codomain:

Inductive mcyl {A B : Type} (f : A -> B) : B -> Type :=
| inl : forall (a : A), mcyl f (f a)
| inr : forall (b : B), mcyl f b
| mseg : forall (a : A), paths (inl a) (inr (f a)).

We can then go through some standard model-categorical retract-argument business to conclude that these two WFS actually form a model structure on the category of types (modulo the defect that it lacks limits and colimits). Peter Lumsdaine has written out a proof.


So far I’ve argued that higher inductive types supply the “missing half” of homotopy theory, and in particular allow us to construct familiar spaces like spheres, tori, projective spaces, Lie groups, etc: anything that can be given a finite cell structure. (With some cleverness, we can probably construct at least some infinite cell complexes as well.) But really, we haven’t even scratched the surface yet, because none of our “higher inductive types” have been “honestly recursive” yet—none of their constructors have taken any inputs from the type being defined!

The most impressive application of “honestly recursive” higher inductive types that I’ve seen so far is the following.

Inductive supp (A : Type) : Type :=
| proj : A -> supp A
| contr : forall (x y : supp A), paths x y.

What does this mean? The type Supp(A)Supp(A) comes with a map proj from AA, and moreover the type Π x,ySupp(A)Paths(x,y)\Pi_{x,y\in Supp(A)} Paths(x,y) is inhabited. But the latter is actually an equivalent way to say that Supp(A)Supp(A) is a (-1)-type, i.e. contractible if inhabited. Furthermore, the elimination rule for Supp(A)Supp(A) says that if BB is another (-1)-type equipped with a map from AA, there is a canonical map Supp(A)BSupp(A)\to B. In other words, Supp(A)Supp(A) is π 1(A)=τ 1(A)\pi_{-1}(A) = \tau_{\le -1}(A), the (-1)-truncation of AA!

I think this is, without a doubt, the cleanest construction of the (-1)-truncation I’ve ever seen; I was very excited when Peter showed it to me. We can apply a similar idea “pathwise” to construct higher truncations as well:

Inductive pi0 (A : Type) : Type :=
| proj : A -> pi0 A
| contr1 : forall (x y : pi0 A) (p q : paths x y), paths p q.

Thus π 0(A)\pi_0(A) has a map from AA and is a 0-type (each of its hom-types are (-1)-types), and is universal among such. We can now define things like

π 1(A,x)π 0(Paths A(x,x))\pi_1(A,x) \coloneqq \pi_0(Paths_A(x,x)) π 2(A,x)π 1(Paths A(x,x),1 x)\pi_2(A,x) \coloneqq \pi_1(Paths_A(x,x), 1_x)

We can use a similar idea to construct a certain amount of quotients, as discussed in the last post. For instance, if RR is an equivalence relation on a set AA, which is in particular a (-1)-type dependent on A×AA\times A, then we might think its quotient should be something like

Inductive quotient (A : Type) (R : A -> A -> NType (-1)) : Type :=
| proj : A -> quot A R
| relate : forall (x y : A), R x y -> paths (quot x) (quot y)
| contr1 : forall (x y : quot A R) (p q : paths x y), paths p q.

This says that Quotient(A,R)Quotient(A,R) is a set (a 0-type) universally equipped with a map from AA and a path relating the images of any two points x,yAx,y\in A for which R(x,y)R(x,y) holds. This should give it the correct universal property in the category of sets, at least, and we might even be able to prove that RR is the kernel of proj:AQuotient(A,R)proj\colon A \to Quotient(A,R). But I don’t immediately see a way to show that this Quotient(A,R)Quotient(A,R) has the right universal property for mapping into types that aren’t 0-types. (On the other hand, if we can be sure that a set having this stronger universal property exists, then it should be equivalent to Quotient(A,R)Quotient(A,R) defined as above.)

In a similar way, we should be able to construct “quotients” of groupoids composed of nn-types, which have the right universal property relative to other nn-types, for any fixed (external) natural number nn; so the only thing standing in the way of constructing all quotients using higher inductive types is infinity. If we allowed higher inductive types with infinitely many constructors, then I have no doubt that we could define honest quotients of any internal groupoid. This gives me a certain amount of hope that once we have a manageable finitary definition of “internal groupoid”, we may be able to use higher inductive types to construct actual quotients thereof.

On the other hand, as far as I can tell, higher inductive types are not subsumed by quotients for groupoids, although they can accomplish some of the same purposes (like truncation, and at least some colimits). For instance, the circle S 1S^1 can be constructed as the quotient of the groupoid 1\mathbb{Z}\;\rightrightarrows\; 1, but constructing a groupoid whose quotient would be S 2S^2 seems no easier than constructing S 2S^2 itself. (Remember that S 2S^2 is not K(,2)K(\mathbb{Z},2)!)


I hope I’ve convinced you that higher inductive types are a fruitful direction for further development of homotopy type theory. However, I want to end with a few caveats.

  1. The formal foundation of this is still a bit in flux. For particular higher inductive types, like the interval, the circle, the mapping cylinders, and so on, we can write down elimination and computation rules that we’re pretty sure are correct. It isn’t appropriate to get into the details here, but you can look at Peter Lumsdaine’s post on the HoTT blog for the form of these rules (including the dependent elimination rules). However, what hasn’t quite solidified yet is a completely general formulation of “a higher inductive type” — what’s allowed, what isn’t, and what elimination and computation rules you end up with.

  2. While we obviously have intuition about what these types should look like in homotopy models, there is work to be done in constructing such types so as to satisfy all the type-theoretic rules. We do know how to find models explicitly in some simple cases. For instance, it’s not hard to show that in the 1-groupoid model of type theory, the groupoid BB \mathbb{Z} satisfies the rules for the circle type.

  3. We need to investigate their computational behavior. In ordinary type theory, computational behavior (such as normalization and termination) is at least as important as the existence of models.

  4. Unfortunately, none of this actually works in Coq or Agda (yet) exactly as written. But we can mostly fake it, by asserting any particular higher inductive type as an axiom, along with its constructors, elimination rule, and computation rules. Some examples are available in Peter’s HoTT post. This is how those of us working on this idea have been formalizing things so far.

    I say we can “mostly” fake it, because in this way we can generally only make the computation rules hold up to homotopy. This is enough for many purposes (although it makes things a good deal more cumbersome), but not for others (in particular, it is insufficient for the proof of function extensionality from an interval type). However, Dan Licata has a clever hack which allows the computation rules for points (but not for paths) to hold on the nose.

Posted at April 24, 2011 5:34 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2391

35 Comments & 0 Trackbacks

Re: Homotopy Type Theory, VI

This stuff is great. I think you guys are coming close to the promised land where logic, \infty-groupoids and homotopy theory become inseparable and even easy to explain.

Posted by: John Baez on April 24, 2011 2:29 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

I’m glad you think so! Maybe we can get that boulder all the way down the hill in our lifetimes. (-:

Posted by: Mike Shulman on April 25, 2011 7:59 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Hmm, sounds like we need a name for someone who’s the opposite of Sisyphus - gently punished by being forced to roll boulders downhill.

Posted by: John Baez on April 26, 2011 1:38 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Cosisyphus?

Then we can speak of homotopy type theory as a “cosisyphean enterprise”.

Posted by: Mike Shulman on April 26, 2011 5:01 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Peter Lumsdaine’s post at the HoTT blog has now appeared; I’ve added links to the main post where appropriate.

Posted by: Mike Shulman on April 25, 2011 8:00 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Sorry if this is a stupid question, but I’m having a little difficulty interpreting some of the definitions here.

So in the definition of nat you say
zero : nat
which I’m reading as “zero is a thing that’s of type ‘nat’” – i.e. zero is a natural number. OK, that’s what I’d expect.

But then in the definition of circle you say
base : circle
where I would expect base to a thing of type ‘point’, not of type ‘circle’. Similarly in the definition of torus. So I can only conclude that I’m misunderstanding what these statements are supposed to be saying.

Is there a simple outline of how this notation works, that covers just enough to be able to follow the definitions in this article?

Posted by: Stuart Presnell on April 25, 2011 1:22 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Just a guess, but….

I’d guess that “base : circle” is a typo and should read “base : sphere”. Yes, base should suggest “point” to you, but we don’t care that it’s intrinsically a point, we care that it belongs to the sphere. Maybe if we had a “point : type” lying around we could have written it as “base : point -> sphere”, but … I don’t know.

(If any of the above are wrong, construe a question mark at the end.)

Posted by: some guy on the street on April 25, 2011 3:24 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Oh… Ooops!

some crossed wires in my memory have just straightened themselves out; specifically, you’re asking about the declaration “base : circle” in the definition of “circle”, where I was worrying about the declaration “base : circle” in the definition of “sphere”. But, again, what “base : circle” means is that “base” belongs to our standard circle which is called “circle”; it doesn’t mean that “base” is a circle (although, I suppose I could be… ). Neither does it mean that “base” is a “circle”. (although, I suppose, that could be, too…)

Posted by: some guy on the street on April 25, 2011 7:03 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

some-guy is correct that base2 : circle was a typo; I’ve fixed it to read base2 : sphere as it should. But base : circle is correct; base is indeed a thing of type “circle”. But recall that a type AA is a space, and a “thing of type AA” is a point of that space. Thus, “a thing of type circle” means a point of the space “circle”.

But I can see that this is confusing! In type theory, one generally denotes a type by the singular name of elements of that type; thus we can read something like x : integer as “x is an integer”, even though it literally means “x is a point of type integer”. However, in homotopy theory, we do not generally name spaces by the singular name of points of that space, because generally there is no common name for such points. If we had a word “splarge” that meant “a point on a circle”, then we could call the type “splarge” and then the declaration base : splarge would mean “base is a point on a circle.” But I think it would be unutterably cumbersome to call the type “PointOnACircle” instead of “circle” so that we could read x : PointOnACircle as “x is a point on a circle” — I think we just need to get used to the fact that there are different ways to name types.

(There is a similar issue in category theory: is the category of sets and functions called “Set” or “Sets” or “Functions”? Most people pick one of the first two, but then we usually inconsistently call the category of sets and relations “Rel”.)

Posted by: Mike Shulman on April 25, 2011 8:44 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Ah, thanks very much, that makes a lot more sense. So the analogy goes:

‘nat’ is the collection of natural numbers
‘circle’ is the collection of points that make up a circle

and

“zero : nat” means ‘zero’ is a member of ‘nat’, i.e. a natural number
“base : circle” means ‘base’ is a member of ‘circle’, i.e. a point on the circle.

Posted by: Stuart Presnell on April 26, 2011 10:15 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Last time you told us that

Coq and Agda also have coinductive types…

Does that mean we may be seeing Tom’s coalgebraic topology running on computers soon?

Posted by: David Corfield on April 25, 2011 2:09 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Well, coinductive types are less general than “coalgebra”, and I don’t think that Freyd’s characterization of the unit interval (for instance) can be implemented as a coinductive type. I believe coinductive types are (weakly) terminal coalgebras for “polynomial” endofunctors, whereas the endofunctor XXXX\mapsto X\vee X used by Freyd is not polynomial.

Posted by: Mike Shulman on April 26, 2011 2:19 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

So what’s allowed? If I’m reading this guide correctly, the coinductive partner of

Inductive nat : Type :=
| zero : nat
| succ : nat -> nat.

just requires us to write coinductive for inductive. Does the following then give us the extended natural numbers?

Coinductive enat : Type :=
| zero : enat
| succ : enat -> enat.

And are we allowed higher coinductive types involving paths?

Posted by: David Corfield on April 26, 2011 9:32 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Alas, no. The coinductive types of Coq are only weakly final coalgebras, so while you can construct objects by corecursion, you don’t get the logical principle of coinduction.

Posted by: Neel Krishnaswami on April 26, 2011 4:56 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

I guess it depends on what you mean by “get the extended natural numbers.” Neel is right that you can’t prove that you don’t get anything “else,” but you do have all the extended naturals inside that coinductive type, correct?

In principle I think one should be able to define higher coinductive types, but we haven’t really thought of any examples yet. Although I have a vague hope that by adding path-constructors to an ordinary coinductive type we could enforce its path-types to be the desired bisimulation relation.

Posted by: Mike Shulman on April 26, 2011 5:23 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Similarly, we can expect to be able to construct any particular kind of finite homotopy colimit.

Ah. We talked about homotopy colimits in HoTT previously (I cannot find the place right now, in the comments to one of the previous posts) and I had gotten away with the impression that you had said it is an open problem how to get them. But maybe that was in a different sense?

I suppose there are two layers here: what you are discussing now is the building of homotopy colimits by hand in terms of ordinary colimits in the given model (say in terms of mapping cones), whereas the previous discussion was probably about conceiving of homotopy colimits genuinely intrinsically to the \infty-topos (or similar) presented by the model.

There is this fun way of thinking about the circle in terms of a homotopy colimit:

S 1* ***. S^1 \simeq \ast \coprod_{\ast \coprod \ast} \ast \,.

One can write down an ordinary pushout of a mapping cone diagram to get a presentation of the intrinsically defined right hand side, and I gather this is what is being encoded by inductive types as you describe above.

But is there an “intrinsic” way to speak of the above homotopy colimit, one that does not involve hard-coded Coq code? (Hope I am saying this right.) My impression was that last time you said: no, there isn’t. Not until we do something to the axioms of HoTT.

Am I remembering that correctly? Or what’s the status of this?

Posted by: Urs Schreiber on April 26, 2011 7:03 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

what you are discussing now is the building of homotopy colimits by hand in terms of ordinary colimits in the given model

I don’t think that’s quite right; we don’t have point-set level colimits in the category of types. This is a particular type-theoretic construction, which (we expect) can be used to construct things that have the right homotopical universal property of (say) a homotopy pushout, or a homotopy coequalizer, but it’s somewhat questionable whether they are determined more exactly than up to homotopy. Or, rather, they are clearly determined a bit more exactly (since the interval says more than being just a point), but how much more is not entirely clear.

Higher inductive types are a fairly new idea, and even if they can potentially solve a given problem, I think it’s still fair to consider such a problem “open” in the sense that there is no standard, accepted, solution yet. I do think HITs are a good solution to the problem of defining particular, finite, homotopy colimits such as homotopy pushouts and homotopy coequalizers.

What I was saying before, I think, is that in order to state and prove (internally) a general theorem of the form “all (even finite) homotopy colimits exist” we would need first a definition of “category”, inside HoTT, in order to index the colimits, which we currently lack. We can prove, externally, that from the finite colimits defined above we can construct all finite colimits, but not as a theorem of HoTT (yet).

There is the same situation in topos theory: in the definition of elementary topos, we assert only some particular finite limits and colimits like pullbacks and terminal objects (or dually pushouts and initial objects – never mind for the moment that in the impredicative case of elementary topoi we can construct colimits from limits). Then we can prove externally (as a statement about elementary topoi, rather than a statement in the internal language of a topos) that an elementary topos has all finite limits and colimits.

But we can also prove in the internal language of a topos a statement like “all limits and colimits exist in the category of sets” where of course internally “the category of sets” refers to the internal representation of the topos itself. This fact, and others like it, are important when viewing a topos as a foundational system for mathematics, rather than an object in some external mathematics which one wants to study. This is the part that’s currently missing from HoTT, until we have at least a notion of “category” to define a notion of “colimit” internally.

I hope this clarifies what I’m saying and what I’m not saying. (-:

Posted by: Mike Shulman on April 27, 2011 8:07 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Then we can prove externally (as a statement about elementary topoi, rather than a statement in the internal language of a topos) that an elementary topos has all finite limits and colimits.

But we can also prove in the internal language of a topos a statement like “all limits and colimits exist in the category of sets” where of course internally “the category of sets” refers to the internal representation of the topos itself.

For the moment I’d be interested in the analogue of the first situation. The urgent immediate question seems to be: Which version of the HoTT axioms describes \infty-toposes? What axioms ensure that a model for the axioms is an \infty-topos? And thus: Do present variants of the axioms ensure that there are, externally, homotopy limits and homotopy colimits?

This is maybe not yet the full realization of HoTT as a new foundation, but it seems important enough that I would like to know to which extent it can be nailed down already:

do you think that a model of HoTT with higher inductive types will have “a good supply” (to be vague) of homotopy limits and homotopy colimits?

Posted by: Urs Schreiber on April 27, 2011 8:38 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Yes, that’s certainly an interesting and important question, although I’m not sure everyone else would describe it as “urgent”. (-: We’ve already proved that plain HoTT has (homotopy) pullbacks and a terminal object, which means it has finite limits externally. Plain inductive types give us coproducts and an initial object, so for external finite colimits it should suffice to show that the “homotopy pushout” I defined above is actually such. I don’t think that should be too hard, but I haven’t tried.

Posted by: Mike Shulman on April 27, 2011 6:21 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

We’ve already proved that plain HoTT has (homotopy) pullbacks and a terminal object, which means it has finite limits externally. Plain inductive types give us coproducts and an initial object, so for external finite colimits it should suffice to show that the “homotopy pushout” I defined above is actually such. I don’t think that should be too hard, but I haven’t tried.

Great, thanks. Can you see if your

  hpushout

will be stable under homotopy pullback?

At the somewhat vague level at which I am following this, it seems to me that this should boil down to something closely analogous to a traditional proof that homotopy pushouts modeled via mapping cylinders are stable, up to weak equivalence, under pullback. Is that right?

Posted by: Urs Schreiber on April 27, 2011 6:40 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Well, we could probably do it explicitly like that, but also, function extensionality should imply that our (,1)(\infty,1)-category of types is locally cartesian closed, so that whatever colimits exist are automatically pullback-stable.

Posted by: Mike Shulman on April 27, 2011 11:23 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

function extensionality should imply that our (∞,1)-category of types is locally cartesian closed,

Ah, right, I missed or forgot that point. You mentioned it in part V. Did you also explain why that is so?

All right, great, so then of the \infty-Giraud axioms remain only two to be checked. One is effectiveness of groupoid objects. The other is the remaining bits of local presentability.

Posted by: Urs Schreiber on April 28, 2011 6:02 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

No, I didn’t say much about why. I think the argument should go like this: the beta and eta rules say that dependent products are right adjoint to pullback at the level of the 1-category of types. So to have an (,1)(\infty,1)-adjunction, we need to know that each of them is an (,1)(\infty,1)-functor, and that the unit and counit are (,1)(\infty,1)-transformations. But function extensionality says basically that functions act on paths, which should be the only nontrivial part. This is admittedly vague. (-:

What remaining bits of local presentability do you have in mind? I haven’t been able to think of any other elementary properties that are versions of local presentability.

Posted by: Mike Shulman on April 28, 2011 6:16 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

A thought occurred to me in a seminar today, having just read Steve Awodey’s claim that

The fundamental groupoid of a space is a logical construction. (p. 72)

Rather than see the homotopy theoretic proof of the fundamental theorem of algebra (if no zero, then polynomial of degree nn is homotopic to both z nz^n and a constant in *\mathbb{C}^{\ast} on large enough circle) as logic + homotopy theory + algebra, could we not see it as homotopy type theory + algebra?

More generally, how will pieces of mathematics bolt on to homotopy type theory?

Posted by: David Corfield on October 18, 2011 4:30 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Could you explain further what you mean by “logic + homotopy theory + algebra”?

Posted by: Mike Shulman on October 18, 2011 6:47 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

It wasn’t a very developed thought. I was supposed to be listening to how we might develop Marx’s notion of ideology. Let me see.

Most people thinking about a proof of the fundamental group of the circle as the integers would understand the movement between lines as cases of logical inference between statements written in the language of topology and homotopy theory. Might we say, and I take it that this is the thrust of Awodey’s comment, that your proof makes it a result of logic, at least to the extent that homotopy type theory is considered a logic?

Then if we have a piece of reasoning which uses homotopy theory, such as the proof of the fundamental theory of algebra, can we ‘absorb’ that into the logic?

Posted by: David Corfield on October 18, 2011 8:54 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Might we say, and I take it that this is the thrust of Awodey’s comment, that your proof makes it a result of logic, at least to the extent that homotopy type theory is considered a logic?

Ye-es… but we might also say that it is a result of chemistry, at least to the extent that homotopy type theory is considered part of chemistry. (-:O

Personally, I don’t find it intuitive or helpful to say that (homotopy) type theory is a logic. I prefer to say (and think) that it is a formal system giving rules for what sorts of judgments we are allowed to write down, and that a certain subclass of those judgments (generally, those acting on (-1)-types) can be called “logic”. This certainly contrasts with the non-type-theoretic (specifically, first-order logic) approach, which is also a formal system giving rules for what sort sof judgments we are allowed to write down, but in which all of those judgments can be called “logic”.

For instance, the theorem that π 1(S 1)\pi_1(S^1) \cong \mathbb{Z} is, classically, shorthand for a logical formula, asserting “there exists an isomorphism…”. But the homotopy-type-theory “proof” does not actually live in the logical fragment of homotopy type theory; instead it directly constructs an inhabitant of the type of isomorphisms. One can then construct from this a proof of the corresponding logical assertion “there exists an isomorphism…”.

I am not a type theorist or logician by training, but I find it more natural to reserve the word “logic” to refer to constructions on propositions and connectives such as “and”, “or”, “there exists”, but not to direct constructions of other mathematical objects. However, if one defines “logic” to mean “whatever formal system of rules we take as basic for mathematics”, then I guess one could say that homotopy type theory is a logic, in contrast with (say) ZFC, which is a set of axioms within a logic (namely, classical first-order logic). But the distinction is at least a bit blurry, since homotopy type theory at least currently proceeds by way of axioms (univalence is currently expressed as an axiom rather than as part of the logic, as are higher inductive types), whereas first-order logic can be expressed either in more “procedural” or more “axiomatic” terms, and I think I recall some debate as to whether, say, the axiom of choice is a law of “logic” or not.

But regardless of whether homotopy type theory is a logic, I’m not sure I would agree that π 1(S 1)\pi_1(S^1) \cong \mathbb{Z} is a “result of logic”, except insofar as everything proven based on a particular logical foundation is a “result” of that logic. Suppose, working in extensional type theory (all types are sets), we defined (laboriously) topological spaces, homotopy, fundamental groups, the circle, and proved that π 1(S 1)\pi_1(S^1) \cong \mathbb{Z} for that circle and that notion of fundamental group. Would that be a “result of logic”? It seems to me that it would be just as much a “result of logic” as the homotopy type theory proof, but at the same time no more a “result of logic” than the same proof performed in classical logic.

However, I could be completely misunderstanding Awodey’s point; that sort of thing happens not too infrequently. (-:

Posted by: Mike Shulman on October 19, 2011 6:19 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Ok, fair enough to be cautious about extending the scope of ‘logic’. So perhaps were I to be selling all this to philosophers, I should adopt the language of Voevodsky in the Oberwolfach report

The broad motivation behind univalent foundations is a desire to have a system in which mathematics can be formalised in a manner which is as natural as possible. Whilst it is possible to encode all of mathematics into Zermelo-Fraenkel set theory, the manner in which this is done is frequently ugly; worse, when one does so, there remain many statements of ZF which are mathematically meaningless. This problem becomes particularly pressing in attempting a computer formalisation of mathematics; in the standard foundations, to write down in full even the most basic definitions–of isomorphism between sets, or of group structure on a set–requires many pages of symbols. Univalent foundations seeks to improve on this situation by providing a system, based on Martin-Löf’s dependent type theory, whose syntax is tightly wedded to the intended semantical interpretation in the world of everyday mathematics. In particular, it allows the direct formalisation of the world of homotopy types; indeed, these are the basic entities dealt with by the system.

Perhaps we should set up a comparison to see which encodings of which theorems are least ugly. Hopefully you have something prettier than Principia Mathematica’s proof of 1+1=21 + 1 = 2.

Posted by: David Corfield on October 20, 2011 11:59 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Hopefully you have something prettier than Principia Mathematica’s proof of 1+1=2.

Inductive nat : Type :=
| zero : nat
| succ : nat -> nat.

Definition one := succ zero.
Definition two := succ one.

Fixpoint plus (n m : nat) : nat :=
  match n with
    | zero => m
    | succ n' => succ (plus n' m)
  end.

Theorem oneplusoneequalstwo : (plus one one = two).
reflexivity.
Qed.
Posted by: Mike Shulman on October 20, 2011 9:59 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

You win, at least judging from Vol 1 of Principia Mathematica. Theorem 54.43 is on page 379. And they haven’t even defined addition yet.

I suppose though that for fair comparison, we’d have to see the whole manual for your system.

Posted by: David Corfield on October 21, 2011 10:34 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Here a heavily belated question (I am only now beginning to look into (higher) inductive types with some seriousness):

allow me to think just \infty-categorically for a second, ignoring all issues of HoTT language, interpretation etc. Suppose then that I have an \infty-endofunctor F:CCF : C \to C on some \infty-category CC. There is an evident notion of \infty-initial \infty-algebras over such an \infty-endofunctor.

Will these be the interpretations of higher inductive types in the internal language of CC?

Posted by: Urs Schreiber on May 11, 2012 9:51 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

That’s a good question! The answer is that it’s a little more complicated, and (I think) better.

Some higher inductive types, such as the 0-level ones (ordinary inductive types) and the “non-recursive” ones (like finite cell complexes), are \infty-initial algebras for \infty-endofunctors. In the 0-level case, this is essentially the content of the Awodey-Gambino-Sojakova paper. In the non-recursive case, these endofunctors are constant (e.g. F(X)=S 1F(X) = S^1 for all XX) and hence kind of boring. Moreover, in order to define them one needs to already have the objects like S 1S^1 in hand. (This is just like how classically, we can see the coproduct A+BA+B as an initial algebra for the constant endofunctor F(X)=A+BF(X) = A+B, which we need to have coproducts already in order to define.)

More general HITs, however, are not initial algebras for endofunctors. I like to think of them instead as presented monads.

An equivalent way to think about ordinary inductive types is as the values of algebraically-free monads on endofunctors. An algebraically-free monad on an endofunctor FF is a monad TT such that the category of TT-algebras (in the monad sense of “algebra”) is equivalent to the category of FF-algebras (in the endofunctor sense of “algebra”). This implies that TT is also free on FF in the usual sense, i.e. involving a left adjoint to the forgetful functor MonadsEndofunctorsMonads \to Endofunctors.

Since the category of algebras for a monad always has an initial object (if the base category does), namely T()T(\emptyset), if endofunctors have algebraically-free monads then they have initial algebras. Conversely, the algebraically-free monad TT on FF can be characterized by saying that T(A)T(A) is an initial algebra for the endofunctor XF(X)+AX\mapsto F(X)+A. In other words, ordinary inductive types are just a convenient way of talking about free monads.

A presentation of a monad with respect to endofunctors, then, should be a realization of it as a coequalizer (in the non-homotopical case) or a more general colimit/codescent-object (in the homotopical case) of (algebraically-)free monads on endofunctors. That is, if ()¯\overline{(-)} denotes the free monad on an endofunctor, we realize TT as a codescent object

F 2¯F 1¯F 0¯T\cdots \overline{F_2} \;\underoverset{\to}{\to}{\to}\; \overline{F_1} \;\rightrightarrows\; \overline{F_0} \to T

Here F 0F_0 is an endofunctor describing the inputs of the point constructors for the HIT, F 1F_1 an endofunctor describing the path constructors, F 2F_2 describes the 2-path constructors, and so on. The fact that we have maps F 1¯F 0¯\overline{F_1} \to \overline{F_0} and not, say, F 1F 0F_1\to F_0 reflects the fact that a path-constructor can construct paths between points that result from iterated applications of the point-constructors, for instance

Inductive X : Type :=
| f : X -> X
| p : forall x:X, (f (f x) == x)

Now an HIT is the initial monad-algebra for such a presented monad, i.e. the object T()T(\emptyset). Of course we can get to all the other values of TT with the +A+A trick above.

I feel like to a category theorist, at least (I can’t say about type theorists), this point of view implies that restricting yourself to ordinary inductive types — initial algebras for free monads — is a weird and artificial restriction. Including higher inductive types is much more natural. (-:

This is also the basic idea of how Peter and I construct models for HITs in our forthcoming paper. The only reason I haven’t mentioned this point of view before is that I’ve only gradually come to understand and appreciate it.

Posted by: Mike Shulman on May 12, 2012 12:57 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

[A] HIT is the initial monad-algebra for […] a presented [\infty-]monad,

That’s great.

I feel like to a category theorist, at least (I can’t say about type theorists), this point of view implies that restricting yourself to ordinary inductive types — initial algebras for free monads — is a weird and artificial restriction. Including higher inductive types is much more natural. (-:

Great, this is what I was wondering about on the nnForum. Very nice, \infty-category theory to the rescue, once more.

Now what I need to do is get some handle on recognizing presentable \infty-monads.

Posted by: Urs Schreiber on May 12, 2012 9:43 AM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

If 1-category theory is any guide, then (κ\kappa-)accessible monads should be monadic over (κ\kappa-)accessible endofunctors, and hence all of them should admit some presentation.

On the other hand, if we limit ourselves to HITs that can be expressed with finitely many constructors, then we can only have presentations that are truncated at some finite level. I don’t know how limiting that is. It does, as we know, suffice to present truncation and localization functors, which are of course idempotent monads (reflectors into subcategories).

Posted by: Mike Shulman on May 12, 2012 5:15 PM | Permalink | Reply to this

Re: Homotopy Type Theory, VI

Then again, now that we know that all HITs are reducible to 1-HITs, we can reduce any such presentation to a 1-truncated one — possibly with infinitely many path constructors. And as long as that infinity of path constructors is “computably” defined, we could then hope to encapsulate it in a finite number of them.

Posted by: Mike Shulman on May 13, 2012 7:25 AM | Permalink | Reply to this

Post a New Comment