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: 'Contextual slice' construction on comprehension categories

Nathan Corbyn (Mar 19 2025 at 11:14):

Hi all! I'm looking for any references pertaining to the following construction:
Let $(p : \mathbb{E} \to \mathbb{B}, P : \mathbb{E} \to \mathbb{B}^\to)$ be a comprehension category, and consider an object $X \in \mathbb{B}$. Define the class of $X$-contextual objects to be the least class containing $X$ and such that whenever $Y$ is $X$-contextual and $y \in \mathbb{E}_Y$, $\mathrm{dom}(P y)$ is $X$-contextual. (Intuitively, this gives objects that can be constructed by performing a finite number of context extensions, starting from $X$). Call the full (replete) subcategory of $X$-contextual objects $\mathbb{B}//X$. I can pull back comprehension structure on $\mathbb{B}$ and I obtain a comprehension structure on $\mathbb{B}//X$.

Nathan Corbyn (Mar 19 2025 at 11:15):

Is this construction known? Does it have a more obvious universal property? (I understand I am describing the full sub-comprehension-category generated by an object)

Rafaël Bocquet (Mar 19 2025 at 13:34):

I am not aware of any reference for comprehension categories.

In the case of categories with families, the contextual slice can be defined as the contextual core of the slice CwF:

$\mathcal{C} // \Gamma = \mathsf{cxl}(\mathcal{C} / \Gamma)$.

The contextual core $\mathsf{cxl}(\mathcal{C})$ of a CwF $\mathcal{C}$ has the following universal property:
for every map $F : \mathcal{D} \to \mathcal{C}$ with bijective actions on types and terms, the inclusion map $\mathsf{cxl}(\mathcal{C}) \to \mathcal{C}$ factors uniquely through $F$. This can also be phrased using an orthogonal factorization system.
(AFAIK, the earliest reference for this is this note of Christian Sattler: https://www.cse.chalmers.se/~sattler/docs/normalization-by-evaluation.pdf)

Moreover, if $\mathcal{C}$ itself is contextual, we have $(\mathcal{C} // \Gamma) \cong (\mathcal{C}[\underline{\gamma} : 1 \to \Gamma])$, where $(\mathcal{C}[\underline{\gamma} : 1 \to \Gamma])$ is the free extension of $\mathcal{C}$ by a new morphism from the terminal object to $\Gamma$.

I would imagine that analogous universal properties can be proven for comprehension categories. The situation is a bit more complicated because comprehension categories form a 2-category while CwFs form a 1-category.

Nathan Corbyn (Mar 19 2025 at 14:38):

Thanks! I think the contextual core operation only makes sense if we have a terminal object but this is not a big assumption

Nathan Corbyn (Mar 19 2025 at 14:41):

Although I suppose one could argue that we could also define $\mathrm{cxl}(\mathcal{C}) = \mathcal{C} // \mathbb{1}$