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: Canonical structure of cwf on Set

Jonathan Arnoult (Jan 06 2025 at 15:29):

Is there anywhere where I can find the proof of the example of the canonical structure of categories with families on the category of sets Set?

More precisely, I'm trying to prove this statement:

the category Set is also canonically a cwf with the functor which to a set X associates the family with $Ty^X$ being the collection of functions $f : Y \rightarrow X$ with $X$ as codomain and $Tm^X_f$ being the set of sections of $f$

found in A Type-Theoretical Definition of Weak ω-Categories from E. Finster and S. Mimram.

I got stuck already when trying to define the action of the substitution on types. If we have $\sigma : Z \rightarrow X$, then $Ty^\sigma : Ty^X \rightarrow Ty^Z$. For $f : Y \rightarrow X$, we need $Ty^\sigma(f)$ to have $Z$ as its codomain, but I don't see any nontrivial function I could choose. $\sigma$ is not necessarily invertible (or even just surjective) so I don't see much what I could do here.

What am I missing?

I had trouble finding a resource online mentioning this very example

daniel gratzer (Jan 06 2025 at 15:56):

So the above description is not precisely a CwF (one would require Ty^X to be a functor, but as written above it's merely pseudofunctorial). A very precise exposition of a 'strictified' version of this CwF structure is described in great detail in Section 3.5 of https://www.danielgratzer.com/papers/type-theory-book.pdf

Roughly, to avoid the issues of pseudofunctoriality, we use the fact that (suitably fiberwise small) families over X correspond to maps X -> U for some grothendieck universe U.

Mike Shulman (Jan 06 2025 at 15:57):

You want the pullback of $f$ along $\sigma$.

However, this isn't strictly functorial, so that description doesn't actually define a CwF literally. (Oh, I see Daniel beat me to it.)

Mike Shulman (Jan 06 2025 at 15:58):

At least if your foundation is a set theory like ZFC, you don't need any universes: you can just define $\mathrm{Ty}^X$ to be the collection of functions from $X$ to the proper class of all sets.

daniel gratzer (Jan 06 2025 at 16:00):

Yep! We try to be a bit careful in the book and universes are a short path to being rather rigorous without delving into too much set theory.. However, they shouldn't be strictly necessary for just type theory!

Jonathan Arnoult (Jan 06 2025 at 16:01):

Oh yes the pullback indeed thanks! Thanks for the reference too, looks like exactly what I needed!

Jonathan Arnoult (Jan 06 2025 at 16:08):

So the cwf with Grothendieck universes would be the canonical one, or are there other cwfs that could claim that title? If so, are they leading to "different" set-theoretic models, so for instance different definitions of $\omega$-categories?