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: learning: questions

Topic: Coherence for categories with limits

Nathanael Arkor (Apr 17 2020 at 14:28):

Are there coherence theorems for categories with (certain classes of) limits analogous to the ones for the various kinds of monoidal categories? Something like "every cartesian category is equivalent to a strict cartesian category" or "every finitely complete category is equivalent to a finitely complete diagram in which pullbacks are strictly associative"? (Though I could imagine the corresponding statements aren't quite as strong.) I couldn't find any references.

Morgan Rogers (he/him) (Apr 17 2020 at 14:30):

When you say "strict cartesian category", in what sense are you asking for strictness?

Nathanael Arkor (Apr 17 2020 at 14:35):

Viewed as a monoidal category, the category is strict: i.e. the associator and unitors are identities.

Reid Barton (Apr 17 2020 at 14:36):

You can just strictify it as a monoidal category then.

Nathanael Arkor (Apr 17 2020 at 14:37):

You aren't guaranteed that the strictified category is also cartesian monoidal, though, right? It simply has to be monoidal and cartesian. But those two structures don't have to coincide, as far as I can see.

Reid Barton (Apr 17 2020 at 14:37):

Also, you don't need to say "cartesian-equivalent" or "lex-equivalent"--equivalences preserve limits.

Reid Barton (Apr 17 2020 at 14:43):

It's still cartesian monoidal because it's monoidally equivalent to the original category, which was cartesian monoidal.

Nathanael Arkor (Apr 17 2020 at 15:03):

Ah, of course, thank you! I had imagined at least one of my questions would turn out to be very simple :grinning_face_with_smiling_eyes:

Soichiro Fujii (Apr 17 2020 at 15:03):

There is the notion of $\tau$-category in Freyd and Scedrov’s book Categories, Allegories; see 1.49 ff. A $\tau$-category is a category with finite limits equipped with a certain set $\tau$ of tables. A table is an ordered sequence $(T;x_1,...,x_n)$ where $T$ is an object and $x_i$ are morphisms from $T$ which are jointly monic.

In a $\tau$-category one has canonical choice of binary products and pullbacks, and there is a unique terminal object. According to 1.49(10) of ibid., canonical products are strictly associative, and canonical pullbacks are compatible in the sense that given any diagram for the pasting law for pullbacks, if the two squares are canonical pullbacks then the outer rectangle is also a canonical pullback. According to 1.4(10)1, for any small category with finite limits $\mathcal{A}$ there exists a “free $\tau$-category” $\mathcal{A}^\tau$ and an equivalence of categories $\mathcal{A}\longrightarrow \mathcal{A}^\tau$.

Nathanael Arkor (Apr 17 2020 at 15:10):

@Soichiro Fujii: that looks perfect, thank you very much!

Thibaut Benjamin (Apr 18 2020 at 13:53):

I don't know if that's of interest for you, but you can also understand categories with families as a trick to present a category with a "split" choice of pullbacks for a certain class of maps. By splits, I mean that when you put two pullbacks squares in the chosen class side by side, the outer square is again a pullback square (that's automatic), but it is also again in the chosen class. I can explain this more in details if you want

Nathanael Arkor (Apr 18 2020 at 14:05):

@Thibaut Benjamin: actually, one aspect I'm not quite clear on at the moment (as these tools are typically used for type theoretic purposes, rather than purely category theoretic) — can we use CwFs to prove coherence results like the above? If so, can we get a stronger result than the one described above in Categories, Allegories?

John Baez (Apr 18 2020 at 17:00):

In general strictifying categories with a chosen set of limits or colimits seems like a fairly pointless business because the universal properties do everything one wants. I think that's why people don't do it very much.

A bit more precisely: having limits or colimits of some sort is a mere property of a category, not extra structure on that category (like a monoidal structure), so the benefits of "improvement via strictification" are much less.

Nathanael Arkor (Apr 18 2020 at 17:05):

@John Baez: it can be important to have strict structure when thinking about type theory, or if you're concerned about getting stricter notions of equivalence. I agree that this isn't a concern to many category theorists, though.

John Baez (Apr 18 2020 at 17:12):

Category theorists consider it to be missing the point of universal properties to want $A \times (B \times C) = (A \times B) \times C$... though when you get to homotopy type theory, you get all these equations in a very elegant way, thanks to the axiom of univalence.

Thibaut Benjamin (Apr 18 2020 at 17:50):

@Nathanael Arkor I'll try to give you a feeling about CwFs, and how they encode strict properties about limits, but I don't know about using them for proving coherence results, nor how it relates to what is described in Categories, Allegories.
First a category with families is an category equipped with a contravariant functor into the families of sets, and given an object $\Gamma$ in a category with families, I denote $\mathrm{Ty}(\Gamma)$ ("types in $\Gamma$") the base set of its associated family, and $\mathrm{Tm}(\Gamma,A)$ ("terms of type $A$ in $\Gamma$") the fiber above $A\in\mathrm{Ty}(\Gamma)$. Given a map $\gamma:\Delta \to \Gamma$, and a type $A$ in $\Gamma$ I denote $A[\gamma]$ the map induced by functoriality on families, applied to $A$. Hence $A[\gamma]\in\mathrm{Ty}(\Delta)$. Now in a category with families, given an object $\Gamma$ and a type $A$, there always exists an object $\Gamma,A$ together with a canonical map $\Gamma,A\to \Gamma$ - these canonical maps are called display maps. There are also other conditions, but I don't want to get too technical because it'll hide the point I want to get to - for my purpose, the thing that is central is the following fact : If I have a object $\Gamma$ together with a type $A\in\mathrm{Ty}(\Gamma)$, you can either form the display map $\Gamma,A \to \Gamma$, or you can apply $\gamma$ to $A$ and get $A[\gamma]$, and then build the dislpay map $\Delta,A[\gamma]$. The axioms of CwF ensure you that these two display maps are related : the display map $\Delta,A[\gamma]\to\Delta$ is the pullback of the display map $\Gamma,A\to \Gamma$ along the map $\gamma$. It is actually a very good way to get used to the formalism of CwF to try and prove this, but I'll assume it here.
The cool thing now, is that if you have two maps $\delta :\Theta\to\Delta$ and $\gamma:\Delta\to\Gamma$, then, by the axioms of CwF, you have that $A[\gamma\circ\delta] = A[\gamma][\delta]$. So for the display maps, this says that $\Theta,A[\gamma\circ\delta]$ is equal to $\Theta[\gamma][\delta]$. With my previous remark on pullbacks, this says exactly that if you stick two pullbacks side by side, or if you compute the pullback of the outer square, you get strictly the same result

Thibaut Benjamin (Apr 18 2020 at 18:00):

I will give an example, which may be more familiar : If you take a contextual category - that is a category with family in which every object is obtained from the terminal object by a succession of display map. ie, every object is written as $A_1,A_2,\ldots,A_n$.
Consider a contextual category in which there is only one type in all contexts. I will denote $\ast$ this type. Then every context is written as $\ast,\ast,\ldots$. Let me write $\underline{n}$ the context of length $n$ - it is clear that there is only one context of each length (and $\underline{0}$ is the terminal object). Then the thing about the pullback I told you shows that the display map $\underline{n+1}\to\underline{n}$ is the pullback of the display map $\underline{1}\to\underline{0}$, along the unique map $\underline{n}\to\underline{0}$. In other words, $\underline{n+1} = \underline{n}\times\underline{1}$ - the equality is strict. You may recognize here a Lawvere theory. The extra terms (which I have not said a lot about) are generate the maps in the Lawvere theory that do not come from products!
In more complicated situations, the intuition is the same : types ensure that some pullbacks exists and compose strictly, terms add extra maps between these pullbacks, and (if you have one) length gives you an analogue of the object being freely generated by the existence of the required pullbacks

Nathanael Arkor (Apr 18 2020 at 20:42):

@Thibaut Benjamin: thank you for the in-depth explanation! I have a little experience with CwFs, though I'm more comfortable with some other models of dependent type theory. I would be interested in knowing precisely how CwFs relate to categories with finite limits with strictly associative pullbacks: I'm not sure if the relationship is clear or not? They certainly seem to have some similar structure.

Nathanael Arkor (Apr 18 2020 at 20:51):

In more complicated situations, the intuition is the same : types ensure that some pullbacks exists and compose strictly, terms add extra maps between these pullbacks, and (if you have one) length gives you an analogue of the object being freely generated by the existence of the required pullbacks

Right, this is how I understand contextual categories. Their precise relationship to finitely complete categories is not obvious to me either, though.

Thibaut Benjamin (Apr 18 2020 at 20:52):

I think the nlab does a pretty good job at comparing. As far as I know, CwF are equivalent to Categories with attributes. There is a notion which is a bit weaker, which is display-map categories. Also there are natural models, which I believe to be equivalent to CwF (to be checked). I think you can make (up to size issues) any category with strictly associative pullbacks into a CwF.
Even better, any category with pullbacks (no need for strict associativity). It is getting late now, but I'll try it out and come back with the construction on Monday

Nathanael Arkor (Apr 18 2020 at 20:52):

That is, it appears that if you have strong enough coherence results for categories with finite limits, you can prove internal language results more straightforwardly, and I would imagine the converse is also true — but I have not seen the results phrased in this way.

Nathanael Arkor (Apr 18 2020 at 20:54):

Also there are natural models, which I believe to be equivalent to CwF (to be checked).

I believe this is the case, though I've never seen this proven.

Thibaut Benjamin (Apr 18 2020 at 20:56):

Btw the best way to familiarise with CwF if you know DTT: objects are "contexts", morphisms are " substitutions", and types and terms are... Well types and terms. Then everything works like in a dependent type theory. You might want to take a look at Dybjer's internal type theory for more details about this

Nathanael Arkor (Apr 18 2020 at 20:56):

Even better, any category with pullbacks (no need for strict associativity). It is getting late now, but I'll try it out and come back with the construction on Monday

That's very kind of you! I admit, till recently I have been focused on simple type theories, so I am fairly new at getting into the dependent side of things :)

Nathanael Arkor (Apr 18 2020 at 20:58):

I've found it a little difficult to build up everything into one coherent picture so far, and there are often hand-wavy explanations of things rather than precise statements in the literature.

Thibaut Benjamin (Apr 18 2020 at 20:58):

I have also an agda formalisation of how a dependent type theory presented as usual, with expressions, and then typing rules, fits into an "internal type theory" which really is the same as a CwF. I'll point you to it!

Nathanael Arkor (Apr 18 2020 at 20:59):

Thibaut Benjamin said:

Btw the best way to familiarise with CwF if you know DTT: objects are "contexts", morphisms are " substitutions", and types and terms are... Well types and terms. Then everything works like in a dependent type theory. You might want to take a look at Dybjer's internal type theory for more details about this

I'm happy enough with this intuition, but as the substitution issues with Seely's original paper demonstrate: it's often easy to miss things just relying on one's intuition.