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

Topic: function extensionality in ∞-categories

Valery Isaev (Aug 19 2021 at 21:37):

Take the category of contextual categories with some additional structure corresponding to some type theory and localize it at homotopy equivalences. Let's call the resulting $\infty$-category the $\infty$-category of models of the given type theory. If we take the type theory consisting only of identity types, $\Sigma$-types, and a unit type, then the $\infty$-category of models of this type theory is equivalent to the $\infty$-category of finitely complete small $\infty$-categories. If we now add $\Pi$-types together with function extensionality, then we should get the $\infty$-category of locally cartesian closed $\infty$-categories. This is still a conjecture, but let's assume it's true.

Now, what will happen if we add $\Pi$-types without function extensionality? I don't think we'll get an equivalent $\infty$-category. Is there some categorical (putative) description of this $\infty$-category?

Mike Shulman (Aug 20 2021 at 00:45):

I would presume it would be something like "weakly locally cartesian closed $\infty$-categories".

Valery Isaev (Aug 20 2021 at 05:27):

Hmm, but what's a weakly locally cartesian closed $\infty$-category?

Nathanael Arkor (Aug 20 2021 at 13:36):

I would imagine a finitely complete $\infty$-category for which pullback has a weak right adjoint.

Valery Isaev (Aug 20 2021 at 15:33):

This might be true if we have only $\beta$-equivalence, but we also have $\eta$ which gives us some form of uniqueness (maybe not the full homotopy contractibility, but still something). This is even more confusing if we add the K axiom. Then we get just 1-categories and the question of uniqueness becomes easier. It seems that we get a bijection between $\mathrm{Hom}(X,B^A)$ and $\mathrm{Hom}(X \times A, B)$. So, do we get locally cartesian closed 1-categories even without function extensionality? Something doesn't add up.

Mike Shulman (Aug 20 2021 at 15:41):

Ah, I didn't realize you wanted to keep $\eta$.

Mike Shulman (Aug 20 2021 at 15:44):

Having $\eta$ but not funext is weird because it means the evaluation map $\mathrm{Hom}(X,B^A) \to \mathrm{Hom}(X\times A,B)$ is bijective on definitional-equivalence-classes of terms, but not an equivalence. So semantically, it's hard to see how to represent it without using a framework like model categories that can distinguish between definitional and typal equality.

Mike Shulman (Aug 20 2021 at 15:46):

The only answer I can think of to guess is something like "weakly locally cartesian closed $\infty$-categories that can be presented by a model category that is actually locally cartesian closed (as a 1-category)".

Mike Shulman (Aug 20 2021 at 15:47):

That sort of answer makes sense in the presence of K too, since a 1-category can also be presented by a model category.