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: theory: category theory

Topic: FOLDS, univalence, and Cisinski model structures

James Deikun (Apr 08 2025 at 06:56):

According to Michael Makkai's FOLDS program (see here), for each finitary direct category $L$, there is a notion of equivalence of presheaves, given by spans of maps that right lift against monos, that preserves satisfaction of sentences and even of open formulas for the rather robust language of FOLDS[$L$]. This notion internalizes to a semantic notion of "intrinsic equivalence" and even a syntactic notion of "internal equivalence" between instances of a fixed telescope of FOLDS[$L$] variables in a given presheaf $M$. Then, taking the $\infty$-categorical realization of the simplicial completion of the minimal Cisinski model structure on $\mathsf{Psh}(L)$ produces a notion of "univalent $L$-space", surprisingly (to me anyway) reflective in $\mathsf{Psh}_\infty(L)$, where the FOLDS equivalence is equivalence in the $\infty$-category and the intrinsic equivalence is "just equality" under the inclusion in $\mathsf{Psh}_\infty(L)$.

James Deikun (Apr 08 2025 at 07:06):

This beautiful story unfortunately breaks down as soon as we no longer have a direct category; it seems to sort of work for the Joyal model structure on simplicial sets but according to Proposition 6.20 of Dimitri Ara's Higher quasicategories vs higher Rezk spaces the Cisinski model structure does not by itself give the correct equivalences for the language of $\omega$-categories. This is because the degeneracies on "triangles" of $n$-globes for $n >= 1$ make it possible to express equality of $n$-globes within the natural "FOLDS language" of $\Theta_m$.

James Deikun (Apr 08 2025 at 07:17):

It seems like it should probably be possible to correct this by moving from $\mathsf{Psh}(L)$ to the category of colax functors from $L^\mathsf{op}$ to $\mathsf{Span}(\mathsf{Set})$ sending monomorphisms to representable spans, which should still be a presheaf category by way of a replacement for $L$, and taking the minimal Cisinski model structure on that. However, that seems like it would be messy and difficult to handle and I wonder if there is any way to recover FOLDS-equivalences directly on $L$-presheaves for non-direct $L$.

James Deikun (Apr 08 2025 at 07:21):

(I'm also interested in any insights on why univalent $L$-spaces turn out to be reflective in ordinary $L$-spaces in the more Makkai-style setup!)

Rafaël Bocquet (Apr 08 2025 at 09:06):

I don't have an answer to your questions, but Makkai's FOLDS can be generalized from direct categories to generalized algebraic theories (GATs); the finitary direct categories correspond to GATs that have only sorts, but no operations or equations. See for instance The language of a model category, talk by Simon Henry and Homotopy Languages, paper in preparation by Cesar Bardomiano and Simon Henry.

James Deikun (Apr 08 2025 at 11:24):

This whole "language of a model category" thing is basically the exact converse of what I want, I want to start with a language and end up with a model category/$\infty$-category where the invariance theorems hold, and where then you can add (non-truncated, well-typed) equality at all types back in because the models of interest are univalent. (Which means this is probably of some help, thanks!)

Mike Shulman (Apr 08 2025 at 15:06):

If you actually look at what Henry is doing, I think he is doing what you do want: starting with a language and creating a model category. He just calls it "the language of a model category" because he claims "most model categories we use in practice" arise in this way, and for those that don't you can basically build an equivalent one that is.

James Deikun (Apr 09 2025 at 01:34):

Okay, I can see where he does that in the talk, it's a lot less obvious from just the article strangely. I tried to model what happens if you encode $\Theta_m$ as a GAT with faces as type constraints and degeneracies as terms and it looks like you still get the monomorphisms as cofibrations and so your language still somehow smuggles in equality on $n$-cells for $n > 0$.

James Deikun (Apr 09 2025 at 01:45):

(Actually now that I think about it it seems really hard and awkward to get this right using cofibrations -- you'd have to have it set up so a walking composable pair of $n$-cells is not a cofibrant object.)

James Deikun (Apr 09 2025 at 01:49):

(The setup Ara uses instead is where an isomorphic pair of parallel $n$-cells is not fibrant for $n > 0$.)

James Deikun (Apr 09 2025 at 07:23):

The replacement for $L$ I was talking about above seems to lead to a subdivision of nerves that splits each $n$-simplex into $2^n$ subsimplices, with all the edges pointing endpoint to midpoint and then from "shorter" to "longer" among the midpoints. It's somewhat related combinatorially to the [[ordinal subdivision]] but different. When you realize the subdivision of a simplex in categories the midpoint of the "longest" edge is the terminal object.

I guess it can be described as "replace the $n$-simplex with the nerve of the poset of closed subintervals of $[0,n]$ under containment". Subintervals rather than subsets making it different from barycentric. And then you squash every backward-facing edge in a cospan corresponding to a monomorphism to the identity, so if you started with all monos you get the same category back.

James Deikun (Apr 09 2025 at 07:37):

(Then once you've made the minimal Cisinski model category, simplicially completed it, simplicially localized it, and optionally taken the homotopy coherent nerve or some realization of it to get an $\infty$-category in your preferred form, you can then do a reflective localization to get rid of the rest of the backward edges.)

James Deikun (Apr 09 2025 at 11:32):

Squishing the backward edges on the monos does not work out "nicely" though, in that if you have a simplex witnessing, say, a nondegenerate face of a degeneracy, where you have a mono composed before a non-mono and the composite is a mono, then the simplex is no longer represented by a poset and you get an unwanted edge crossing the cospan and representing the degeneracy itself. And all degeneracies in a reasonable indexing category have a nondegenerate face! This evidently requires more thought.

James Deikun (Apr 09 2025 at 17:53):

I spoke to Simon Henry by email and he cleared up some confusion I had about Theta categories. The boundary inclusions of the free strict $n$-categories on the thetas are not cofibrations of strict $n$-categories in the canonical model structure, so the Theta nerve of strict $n$-categories seemingly isn't a reasonable representation of the category of $n$-categories for putting the coclan factorization structure induced from the canonical presentation on it.

Apparently people have written up a nerve construction that uses a Reedy fibrant replacement of the co-Theta-object of free strict $\omega$-categories on thetas, but he can't remember who and I can't seem to google it up, does anyone here know about it?

James Deikun (Apr 09 2025 at 20:03):

Apparently it's Campbell A homotopy coherent cellular nerve for bicategories for bicategories and we still don't have the one for $\omega$-categories if it even exists. Still, this is kind of cool; it constructs the bicategories from the strict 2-categories using cofibrant replacement to create the proper homs. This isn't enough to construct the weak $\omega$-categories from the strict ones since there aren't even enough models in that case, but it can construct the subcategory of strictifiable weak $\omega$-categories probably.

James Deikun (Apr 09 2025 at 20:29):

Also by examining the way identity works in the FOLDS theory of 1-categories, I think I figured out the replacement thing finally. Are you ready? Take the nerve of the category $L$, and in each simplex, mark the edges that are monomorphisms. This equips each simplex with a planar forest, given in pre-order by the spine ordering, of which the marked edges are the transitive closure. Take all the pre-order intervals in the tree, close them under ancestry (toward the roots), and take the preorder (the other kind) under inclusion. Glue all these preorders together to get your new category $L'$.

James Deikun (Apr 11 2025 at 10:16):

Building on the Homology Languages paper, it seems like it would make sense to define an arity of a clan $C$ to be a dense generator $\mathcal A$ of the dual of the underlying category, that extends via Yoneda to a dense generator of the category of models, equipped with a set of fibrations $\mathcal I$ whose image under Yoneda generates the WFS. I think this data allows you to recover a much more reasonable presentation of a clan as a Cartmell theory.

James Deikun (Apr 11 2025 at 10:36):

Meanwhile what I want to do is define a Cartmell theory as "free" if it doesn't use any equality axioms (free theories should have univalent models in spaces), and an arity as "eleutheric" if it is compatible in some way with a free resolution--if it already sees where the syzygies land. However, by the nature of a Cartmell theory where a term or type could need an equality axiom for its definition to be well-typed, creating a free resolution of one is already as hard as the whole problem I want to solve. (Like, I think you could read a homotopic weakening of the theory right off of a free resolution if it's stable under the introduction of new types.) So I'd like it if there's an easier way to define "eleutheric" through some kind of closure property.