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.

March 5, 2013

Category Theory in Homotopy Type Theory

Posted by Mike Shulman

Benedikt Ahrens, Chris Kapulkin, and I have just posted the following preprint:

This is mainly a development of basic (1-)category theory using homotopy type theory (a.k.a. “univalent foundations”) as the foundational system. So for all of you readers who’ve been enjoying the posts with vague waffly discussions of type theory, and longing for something to sink your teeth into, this may be a good start.

The paper has two parts. One is written in LaTeX like a traditional math paper, using English sentences and an informal style, with “abuses of notation”, leaving trivial things to the reader, etc. However, even this part is different from most informal mathematics in that it is founded in type theory rather than (some variety of) set theory. If you’ve read this post and this post you may have some idea of what that means. Section 2 of the paper gives a very brief introduction to it, as well as to the aspects that are special to homotopy type theory (versus other kinds of type theory). We would very much appreciate feedback on readability.

The second part of the paper is a formalization in the proof assistant Coq. (This shows up as the “ancillary files” on the arXiv.) The informal and formalized parts are vaguely parallel: though they don’t match up exactly, the same main theorems occur in both. A brief discussion comparing them is in Section 9 of the informal paper. The Coq development is based on Vladimir Voevodsky’s “Foundations” library, which was the first library for doing homotopy type theory in Coq. (We’re hoping to update it later to use the new “second generation” version of the HoTT library that’s currently under development at IAS.)

Okay, enough meta, what is this paper about?

The main novelty when doing category theory in homotopy type theory is that you have more freedom in how you treat equality of objects in a category. The obvious definition of a category AA has a type of objects, say A 0:TypeA_0:Type, and a family of types of morphisms, say hom A:A 0×A 0Typehom_A : A_0 \times A_0 \to Type. For simplicity, we restrict ourselves to 1-categories, in which case we should require each type hom A(x,y)hom_A(x,y) to be a set in the precise sense of homotopy type theory (i.e. a 0-truncated type, containing no higher homotopy). But what sort of type should A 0A_0 be? The choice we make governs how equality of objects in AA gets treated.

If we require A 0A_0 to also be a set, then we get a notion of “category” which behaves more like categories in traditional set-theoretic foundations. In such categories, we can compare objects for equality, and this “equality” behaves basically like equality always has in set theory. (In particular, two objects can be equal in only one way.) This sort of equality of objects is, in particular, stricter than isomorphism. Thus we can have objects that are unequal but isomorphic, and we can perform constructions that violate the principle of equivalence. Following Toby Bartels, we call this sort of category a strict category.

Another option, however, is to require A 0A_0 to be a 1-type (that is, a 1-truncated type, behaving like a 1-groupoid) in which equality is identified with isomorphism in the category AA. More precisely, consider the equality type Id A 0(x,y)Id_{A_0}(x,y), which is defined for any x,y:A 0x,y:A_0. Remember that in homotopy type theory, equality in general types behaves like paths in a space or equivalences in a higher groupoid, so that two points can be equal in more than one way. In this case, the equality type of A 0A_0 comes with a canonical map idtoiso:Id A 0(x,y)iso A(x,y)idtoiso: Id_{A_0}(x,y) \to iso_A(x,y) into the set of isomorphisms from xx to yy in the category AA (defined in the usual way) — we define this by “path induction”. We say that a category is saturated or univalent if this map idtoisoidtoiso is an equivalence, for all objects xx and yy.

The name “univalent” refers to the fact that this is closely related to the univalence axiom. Specifically, the univalence axiom implies that the category of sets is saturated/univalent. Just as the univalence axiom identifies equality of types with equivalence, saturation for a category identifies equality of objects with isomorphism. One must emphasize, however, that relative to set theory, it does this by expanding the notion of “equality” to coincide with isomorphism, rather than restricting the notion of isomorphism to coincide with equality.

Saturated categories always satisfy the principle of equivalence. Any construction we can perform in type theory must respect the equality types — that’s essentially what the principle of path induction says. Thus, since in a saturated category, equality of objects is identified with isomorphism, it follows that any construction we can perform must also respect isomorphism of objects. So working with a saturated category provides an ironclad guarantee of “non-evilness”: if you can state your definition or prove your theorem for saturated categories in HoTT, then it is automatically isomorphism-invariant.

Saturated categories also satisfy their own, categorified version of univalence: if two saturated categories are equivalent (in any of the the usual senses of “equivalence of categories”), then they are equal. Thus, any construction on saturated categories must also satisfy the principle of equivalence. There is no notion of “equality” or even “isomorphism” of saturated categories that is stronger than equivalence.

Saturated categories have other good properties as well. For instance, consider the statement “every fully faithful and essentially surjective functor is an equivalence of categories”. In classical set theoretic foundations, this statement is equivalent to the axiom of choice. The same is true for strict categories in HoTT. However, for saturated categories, this statement is just true, without the need for any axiom of choice. It’s essentially a “functor comprehension principle”, or a categorical version of the “principle of unique choice”: if something is determined up to unique isomorphism, then by univalence it’s determined up to unique equality, and hence we don’t need any axiom of choice in order to choose it.

The thing which I like so much about this approach is that it allows multiple kinds of category theory to coexist. People who prefer to “speak no evil” can work with saturated categories, and almost all of classical category theory will work just as it does classically (or even better), since it is well-known to satisfy the principle of equivalence. On the other hand, the occasional naturally occurring examples of strict categories, such as Peter May’s by-now classic example, are not excluded through philosophical prejudice, but merely recognized as a different sort of category, one in which we have, and care about, a notion of equality for the objects which is stricter than isomorphism. Such categories seem to be rarer than univalent ones, but they are not nonexistent.

Strict categories and saturated categories live together in the world of “categories” that have no restriction imposed on their types of objects. We call these latter “precategories”, suggesting that they are the “raw material” from which one can obtain other notions of category (strict, saturated, …) by imposing conditions that determine the paths in the type of objects.

There are other possibilites as well, although we didn’t mention any of them in the paper. For instance, it is natural to consider \dagger-categories which are “\dagger-saturated”, meaning that the equality type between objects is identified with the type of unitary isomorphisms. Whatever sort of category we are considering generally determines the right notion of “sameness” between its objects, and we can then impose an axiom on our precategories identifying that notion of sameness with the equality type, ensuring that all constructions are invariant under the correct kind of sameness.

Sometimes, however, it may happen that a precategory arises naturally whose equality types are “wrong” for what we want them to be. For instance, there is a “homotopy precategory” of types, whose type of objects is the universe TypeType, and whose hom-sets are hom(A,B)=π 0(AB)hom(A,B) = \pi_0(A\to B), the 0-truncation (reflection into sets) of the function types. We might want to treat this category category-theoretically, but it is not saturated. For this reason we may want a “saturation” operation on precategories. This is the main theorem in the paper which has no counterpart in classical category theory.

There are (at least) two ways to construct the saturation of a precategory. The first is with a higher inductive type: we define the new type of objects A 0^\hat{A_0} to be generated by the original type of objects A 0A_0, together with a path for every isomorphism in the original category AA, satisfying appropriate laws and truncation axioms, all of which can be expressed as higher path constructors. We didn’t do this in the paper, first because it’s long and tedious to do carefully, and second because Vladimir’s library isn’t designed for HITs.

The other way is with the Yoneda embedding. Since the category of sets is always saturated, it follows that so is any presheaf category. Thus, if we take the full image of any category inside its presheaf category, we obtain a “weakly equivalent” category which is saturated, and which is the saturation of the original category. This approach is easier to describe, although has the disadvantage of not preserving smallness.

In the paper, we call this saturation operation the Rezk completion, because it is essentially a truncated version of the replacement of a Segal space by a complete Segal space. Indeed, in the model of homotopy type theory in simplicial sets, we can almost identify precategories, strict categories, and saturated categories with 1-truncated versions of Segal spaces, Segal categories, and complete Segal spaces respectively. (The term “precategory” comes from this world as well — it was suggested in an nForum discussion as a name for “Segal space objects” internal to an (,1)(\infty,1)-category.)

On the other hand, in higher topos semantics, strict categories are basically internal categories in a 1-category of sheaves (of sets), while saturated categories are stacks, and the Rezk completion is the stack completion.

So the notion of saturated/univalent category not only unifies philosophical divides in ordinary category theory, it matches them up with appropriate definitions of higher category and higher stacks.

Posted at March 5, 2013 4:04 AM UTC

TrackBack URL for this Entry:

24 Comments & 0 Trackbacks

Re: Category Theory in Homotopy Type Theory

You folks make a somewhat astounding (to me) observation on page 5, when you define the propositional truncation A:=Π(P:Prop).(AP)P \|A\| := \Pi (P : \mathrm{Prop}).\; (A → P ) → P

You first note that this is impredicative, which makes sense to me, and then you make the amazing claim that it can be defined as a higher inductive type without any impredicativity.

How does that work? The type A\|A\| must have a single term constructor taking an AA, but I can’t quite figure out what the path constructor(s?) for it look like.

Posted by: Neel Krishnaswami on March 5, 2013 11:43 AM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

The path constructor has type Π(x,y:A),x=y\Pi(x,y:\Vert A\Vert),\, x=y. The propositional truncation is called supp here and isInhab here. I’ve gotten so used to this by now, but I agree that it is amazing! That the propositional truncation can be defined this way is an insight due to Peter Lumsdaine; it was the first interesting example of a “properly recursive” HIT.

Posted by: Mike Shulman on March 5, 2013 1:30 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

That’s an extremely pretty and direct way of expressing proof anonymity! Even better, it looks like you can derive 00\|0\| \to 0, which is often a problematic entailment in proof irrelevance modalities.

Now to see what surprises you have in pages 6 and further…. :)

Posted by: Neel Krishnaswami on March 5, 2013 2:17 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

Why is 00\Vert 0 \Vert \to 0 problematic? It seems to me like since 00 is a mere proposition, any reasonable notion of “proof irrelevant modality” ought to factor 000\to 0 through 0\Vert 0\Vert.

Posted by: Mike Shulman on March 5, 2013 2:21 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

Semantically, of course you’re right.

The difficulty has been in getting the proof theory to go along (that is, supporting normalization/cut-elimination). Since proof irrelevance is still computationally interesting even without this entailment — e.g., for guiding program extraction from dependently-typed proofs — there has been a fair amount of work on versions of proof irrelevance which do not permit deriving this implication.

See for instance Andreas Abel and Gabriel Scherer’s On Irrelevance and Algorithmic Equality in Predicative Type Theory.

So it seems that any solution to the problem of normalization for higher inductive types also solves en passant the problem of normalization for proof irrelevance modalities.

Posted by: Neel Krishnaswami on March 5, 2013 3:02 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

I believe that Licata-Harper 2TT solves the normalization problem for one univalent universe of 0-types, as well as some higher inductives, when all types are 1-types. I know they’ve done the circle; I suspect that it would work just as well for the propositional truncation.

Posted by: Mike Shulman on March 5, 2013 5:09 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

I’ve remarked before (and Mike reasonably replied that it looked like classical homotopy more than type theory, because it is) that IsInhab A is the self-join algebra Inh AInh_A generated by AA, meaning it is defined to have a map Inh AInh AInh A Inh_A \star Inh_A \to Inh_A interpolating the identity maps on either edge. So it is the classic “infinite self-join” of AA, whose contractible-if-nonempty property is behind the Ganea+Milnor delooping constructions and certainly lots of other things.

Posted by: Jesse C. McKeown on March 5, 2013 2:23 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

Your construction of the so-called “Rezk completion” is a nice application of yoneda, it seems. Interestingly, this is completely different than the construction I used for complete Segal spaces, which is basically a generalization of a classifying space construction.

Can this kind of classifying space construction be made to work in your theory? It feels more “constructive” than what you actually do. I’d guess there are at the very least troubles with handling arbitrarily higher-homotopies, which are implicitly part of the construction of a classifying space.

Posted by: Charles Rezk on March 5, 2013 2:40 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

Yes, an alternative classifying-space-style construction is what I referred to above using higher inductive types. There would be higher-homotopy problems in doing this for (,1)(\infty,1)-categories, but with 1-categories it is not a problem since we can cut off at a finite level. Define A^ 0\hat{A}_0 to be the higher inductive type generated by:

  • A function i:A 0A^ 0i:A_0 \to \hat{A}_0.
  • For each isomorphism f:xyf:x\cong y in AA, an equality j(f):i(x)=i(y)j(f):i(x) = i(y) (making isomorphisms into equalities).
  • For each equality p:x=yp:x=y in A 0A_0, an equality j(idtoiso(p))=i(p)j(idtoiso(p)) = i(p) (if an isomorphism is already an equality, don’t throw in a new one).
  • For each x:A 0x:A_0, an equality j(1 x)=idpath i(x)j(1_x) = idpath_{i(x)}
  • For each f:xyf:x\cong y and g:yzg:y\cong z, an equality j(gf)=j(g)j(f)j(g\circ f) = j(g) \cdot j(f).
  • A “truncation constructor” analogous to the one mentioned above, which forces A^ 0\hat{A}_0 to be a 1-type: for each x,y:A^ 0x,y:\hat{A}_0, each pair of equalities p,q:x=yp,q:x=y, and each pair of equalities r,s:p=qr,s:p=q, an equality r=sr=s.

I agree that this approach is more “constructive”, and it also has the advantage that it doesn’t increase the universe level (assuming A 0A_0 belongs to a universe which is closed under HITs). But it’s a bit more tedious to construct hom A^(,)hom_{\hat{A}}(-,-) and prove the universal property this way, since you have to do longish double case analyses on all the constructors of A^ 0\hat{A}_0.

Posted by: Mike Shulman on March 5, 2013 2:58 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

I look forward to Charles bashfully referring to it as the

so-called “Rezk completion”

for many years to come. (What else is a modest chap to do?)

Posted by: Tom Leinster on March 5, 2013 3:04 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

Don’t be modest, Charles. Own it!

(I wish I could track down the story I heard: when someone asked Marston Morse what he was working on these days, he proudly said, “My Theory!”)

Posted by: Todd Trimble on March 5, 2013 3:55 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

Okay, I will. It’s my theory, and it belongs to me!

Now I’m reminded of the Monty Python skit about the Theory of the Brontosaurus …

Posted by: Charles Rezk on March 5, 2013 8:44 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

I just had occasion to look at Coxeter’s paper My Graph (about, inter alia, the Coxeter Graph—and what a fine paper it is too), and noticed that, despite the title, he referred to the graph in question as “the so-called Coxter graph” in both the abstract and at its first mention in the main text (and in quotes at its second mention). So one can mix and match!

Posted by: Tim Silverman on March 13, 2013 12:13 AM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

I have witnessed John Cardy calling Cardy’s formula “my formula”.

Posted by: Tom Ellis on March 15, 2013 11:54 AM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

a different sort of category

I don't think of strict categories as a different sort of category so much as a (saturated) category with extra stuff, specifically a category equipped with an additional fine notion of equality of objects. This may be hard to say in HoTT, where a category already has a notion of equality of objects which is simply [I almost wrote ‘merely’] isomorphism, but there is another way to put it: A strict category CC is a category WW equipped with an essentially surjective functor from (the discrete category on) a set OO.

Then if I understand correctly, a precategory CC is a category WW equipped with an essentially surjective functor from an \infty-groupoid OO. And in the same vein, a saturated category CC is a category WW equipped with an essentially surjective functor FF from a 11-groupoid OO, with the additional property that FF is fully faithful on isomorphisms (and so makes OO equivalent to the core of WW, so the concept of saturated category is equivalent to the concept of category).

This doesn't take away from the pluralism of allowing both strict and saturated categories. Some categories come to us with an interesting strictness structure, and some don't, that's all.

Posted by: Toby Bartels on March 8, 2013 5:57 AM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

There are also situations where we impose such “strictness structure” somewhat artificially which is awkward but very convenient. Here, I’m thinking of Reedy categories. We typically define them in a way that implies that they are skeletal even though the end result of constructions that we care about (factorizations, lifts) is invariant under equivalence. In this traditional approach things would become rather messy if we didn’t insist on skeletality. I wonder whether in HoTT we can see Reedy categories as saturated categories and still carry out typical arguments in a neat way. I’m guessing that the answer should be “yes” since notions of “equality” and “isomorphism” of objects are now unified, but I don’t see how that would work so I’d appreciate if someone could elaborate.

Posted by: Karol Szumiło on March 8, 2013 6:28 AM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

That sounds like an interesting idea! But I suspect you may have to do the elaboration of your idea yourself. (-:

Posted by: Mike Shulman on March 8, 2013 2:47 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

Oh, I see. For some reason I presumed that people were already thinking about Reedy type arguments within HoTT.

Posted by: Karol Szumiło on March 8, 2013 3:25 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

People are thinking about Reedy diagrams on inverse categories, but I don’t know of anyone thinking about more general Reedy ones, at least not internally. Having degeneracies around makes functoriality much harder.

Posted by: Mike Shulman on March 8, 2013 4:48 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

The issues I mentioned are present already for inverse categories. Let’s say you have a category equivalent to an inverse category but not necessarily skeletal. If you inductively construct a diagram over it, you may be forced into an awkward case distinction depending on whether an object considered at the moment is isomorphic to an object considered previously or not. I expect that in HoTT such a case distinction should disappear.

Posted by: Karol Szumiło on March 8, 2013 8:52 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

Well, yes, but I think so far the presentations of inverse categories we’ve used have had the well-founded relation on objects built in. For instance, we’ve thought a lot about the semisimplicial indexing category, where the objects are just the natural numbers. More generally one can think about inverse categories defined inductively in stages. I don’t know of anyone having worried about starting with an abstract category and separately giving a proof that it’s inverse, rather than having the inverse-ness built into the data.

Posted by: Mike Shulman on March 8, 2013 10:10 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

I’m not really interested in distinguishing between the phrases “a category equipped with some extra stuff” and “a different kind of category”.

Posted by: Mike Shulman on March 8, 2013 2:45 PM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

Hello, until today I had heard of a Saturated category. Very interesting. I have been publishing on categorial model saturation on categories since ASL Summer Colloquium Sofia, for example: Frgament Ultraproduct Models on Projective Sets Cyrus F Nourani* October 2012- published July 2012. I, of course was lurred to mathematical models years ago and have published on Martin-Lof type constructions over a decade ago. Cheers, DE and SFU, Burnaby.

Posted by: Cyrus on May 10, 2013 10:34 AM | Permalink | Reply to this

Re: Category Theory in Homotopy Type Theory

PS that was ” I had’nt heard” :-))

The saturation notions are not the same perhaps a far-fetched generalization now.

I stumbled on this Cafe today when I went to get a link on what glimpse I can give on Homotopy for a new manuscript. I had not planned to say so much on that topic now. Later :-)) Cheers

Posted by: Cyrus on May 10, 2013 11:52 AM | Permalink | Reply to this

Post a New Comment