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: freely adding comprehensions

Mike Shulman (Jan 15 2022 at 02:02):

If $P:T^{\rm op}\to \rm Cat$ is a hyperdoctrine with at least products in the fiber categories, then there is a way of "freely" adding Lawvere-style comprehension to it. The base category $T^+$ is the Grothendieck construction of $P$, with objects $(x\in T, a\in P(x))$, and the fiber category $P^+(x,a)$ is the Kleisli category of the comonad $a\times -$ on $P(x)$: its objects are those of $P(x)$, while a morphism from $b$ to $c$ in $P^+(x,a)$ is a morphism $a\times b\to c$ in $P(x)$. The comprehension of $b$ in this fiber category is $(x, a\times b)$. (If the categories $P(x)$ are posets, then $P^+(x,a)$ is equivalent to the slice $P(x)/a$.)

What is the best citation for this construction? The posetal case is described in detail in https://arxiv.org/abs/2108.03415 which says it is "recalled" from https://arxiv.org/abs/1206.0162. The latter in turn attributes it to Jacobs' 1999 book Categorical Logic and Type Theory but without any more specific reference, and I haven't been able to find it therein. Note that the question isn't just about the Grothendieck construction of a hyperdoctrine for a base category, but about the new hyperdoctrine that we can define over it.

Mike Shulman (Jan 17 2022 at 01:33):

Crossposted to MO