Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: practice: software

Topic: formalizations of categories

James Deikun (Sep 20 2021 at 21:36):

I'm looking for help finding, or if necessary creating, the best formalization of 1-category theory. In the past I have run into some nearly insurmountable problems dealing with 1-category theory in Agda or Coq with existing libraries:

• If you have quotients as an axiom, and do everything with sets, everything is stuck all over the place.
• If you use setoids for homsets, then constructions like functor categories and arrow categories don't work correctly because they have too strict an equality on objects.
• If you use setoids for homsets and for the collection of objects, there are an unmanageable number of proof obligations for creating a category and equality of objects is too weak to provide coherent composition of diagrams fused along equalities.

So getting this right involves either a trick I don't know about, or a proof assistant that can provide better support for quotient types in the metatheory ... does anyone have suggestions/experience with this?

James Wood (Sep 20 2021 at 21:55):

agda-categories takes the second approach, but seems to handle those examples well enough. I'm not sure what the problem with functor categories would be, and arrow categories are at https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Construction/Arrow.agda.

James Wood (Sep 20 2021 at 22:08):

If there's a trick to these sorts of categories, I think it's that, surprisingly, it's not the equality of objects from 𝓒 that you have to worry about in Arr(𝓒), but rather the equality of equations from 𝓒. But equality of such equations is trivial, so there is nothing to worry about.

Alex Gryzlov (Sep 20 2021 at 22:09):

Take a look at https://arend-lang.github.io/ maybe? It's based on HoTT and has some categorical stuff in stdlib

James Deikun (Sep 20 2021 at 22:10):

The problem with arrow categories is that equal arrows in $\mathcal{C}$ become unequal objects in $Arr(\mathcal{C})$ ... with functor categories it's that the proofs can become part of what is compared for equality (Agda has ways around that, Coq doesn't particularly).

James Deikun (Sep 20 2021 at 22:14):

In almost all cases these problems don't prevent you from doing a basic construction, but once you start doing proofs around it you find that you are demanded to prove equalities that either shouldn't be necessary, or that should be necessary but aren't true.

James Wood (Sep 20 2021 at 22:16):

Ah, yeah, it makes you really commit to working up to equivalence of categories. But it should be possible to maintain that invariant. agda-categories has some decent experience behind it these days.

James Deikun (Sep 20 2021 at 22:17):

My latest case was trying to prove the nerve theorem for categories in Coq, where I could extract all the arrows in the spine of a horn but couldn't prove that they connect into a composable string.

James Deikun (Sep 20 2021 at 23:02):

Can you prove the nerve theorem in agda-categories? I don't recall it being in there.

Jacques Carette (Sep 21 2021 at 14:35):

The nerve theorem has not been proved in agda-categories. Do you have a canonical reference?

Jacques Carette (Sep 21 2021 at 14:39):

I don't understand your problem with $\mathsf{Arr}$? Equivalent arrows before equivalent arrows, which is all you can ask for in weak category theory. And agda-categories takes the weak approach throughout.

James Deikun (Sep 22 2021 at 19:45):

Jacques Carette said:

The nerve theorem has not been proved in agda-categories. Do you have a canonical reference?

The reference I've been using is Lurie, Higher Topos Theory Proposition 1.1.2.2 (pp. 9-11) but it's hardly canonical. I've worked on it a bit at https://github.com/xplat/agda-categories/tree/nerve-theorem but I've run into some trouble getting the levels to match up in the definition "$\Delta$-yoneda" without reproving the Yoneda lemma from scratch, and the part that will use it is just a mess for now ...

Jacques Carette (Sep 22 2021 at 23:50):

Thanks for the link. Some of the local fixes you've done in that branch are nice, and would be worth a PR on their own (please!). Otherwise, I'm not seeing anything obvious, I'd need to bring it up in Agda to dig a bit deeper. If you want a hand, shout, I'll see what I can do.

James Deikun (Sep 23 2021 at 02:33):

The more I look at it the more it looks to me like I can't use the existing proof of the Yoneda lemma and I can't generalize the existing proof without restructuring it so that it's originally proved with an explicitly universe-lifted Yoneda embedding and the proof for the bare Yoneda embedding is backed out of that. It would be really nice to have universe cumulativity in Agda so that Agda wouldn't (and you wouldn't have to) keep track of how many times you lifted things to a higher universe ...

Jacques Carette (Sep 23 2021 at 12:08):

Jason proved some lifted version - maybe in Yoneda.Properties?

Yoneda is so important that having alternate proofs is not a bad idea, especially with slightly different assumptions on universes.

Reid Barton (Sep 23 2021 at 12:53):

The nerve theorem is about small categories. Of course if you accept the universe axiom then every category is small in some universe, but the point is that the nerve theorem describes those simplicial sets which arise as the nerves of $\mathcal{U}$-small categories; it doesn't say anything about the nerves of $\mathcal{U}$-small and locally $\mathcal{V}$-small categories. This is kind of intrinsic in the whole idea of the nerve (and the simplicial approach to (higher) category theory in general), which puts strings of $n$ composable arrows on the same footing for all $n$, including $n = 0$ and $n = 1$.
So, for formalization it would be appropriate to assume from the start that all the universes parameterizing your categories are equal.

Reid Barton (Sep 23 2021 at 13:11):

The next issue would be: how do you even define the nerve of a category whose "homsets" are actually setoids, if you can't form quotients?

You could just ignore the relations between morphisms, but then the nerve won't satisfy the unique lifting condition (for $n = 3$) of the nerve theorem, and in any case it seems like the wrong thing to do.

A better idea would be to recognize that we actually have a simple kind of 2-category and define the nerve to be the Duskin nerve. Then I guess you should be able to prove a nerve theorem, but it won't be the same as the one for 1-categories: the filler of a horn $\Lambda^2_1$ won't be unique.

It might also be preferable/necessary to regard the nerve as taking values in simplicial setoids, although there is something a bit strange here, because the objects of your category (which will be the 0-simplices of the nerve) actually do form a set. But a set is a special kind of setoid, so this isn't necessarily a deal-breaker.

Reid Barton (Sep 23 2021 at 13:13):

This is basically all to say: this is one of the foundational places where all the differences between the notion of category in classical mathematics and the one in agda-categories really play a big role, and you'd better begin by figuring out what nerve construction is even possible and what the correct nerve theorem will be for this new concept.

Reid Barton (Sep 23 2021 at 13:17):

Essentially the same issues arise when you want to define the equivalence between the two descriptions of categories, one in the "dependently typed" style with sets $\mathrm{Hom}(A, B)$ of morphisms for each pair of objects $A$, $B$, and one with a single set containing all the morphisms of the category (the description of Cat as the models of an essentially algebraic theory).

Reid Barton (Sep 23 2021 at 13:18):

The nerve construction is very close to the latter description.

James Deikun (Sep 23 2021 at 13:20):

I went with having simplicial setoids. I figure the extra universe level for objects might result in needing a smallness side condition of some kind on the nerve theorem but I'm hoping I can figure that out as I go.

James Deikun (Sep 23 2021 at 13:22):

Fortunately for this approach simplicial "sets" in agda-categories are already simplicial setoids! But I was using the same approach in Coq when I was defining simplicial sets from scratch.

Reid Barton (Sep 23 2021 at 13:23):

By simplicial setoids do you mean strictly simplicial setoids, or "pseudosimplicial setoids"? i.e. when we compose the actions of maps of $\Delta$, we could require commutativity only up to the relation.

James Deikun (Sep 23 2021 at 13:25):

If I understand your meaning correctly, the latter. The actions take values in maps of setoids.

Reid Barton (Sep 23 2021 at 13:30):

Then in the nerve theorem, I guess you have to interpret "unique" lift as meaning unique in the setoid-sense, i.e., there is a lift and every lift is related to that one.

Jacques Carette (Sep 23 2021 at 13:32):

(As a very interested bystander: thanks @Reid Barton for a very illuminating description of the issues)