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$.)

Does anyone know an original citation for this construction? The posetal case is described in detail in Trotta - An algebraic approach to the completions of elementary doctrines which says it is recalled from Maietti and Rosolini - Elementary quotient completion. 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, but about the new hyperdoctrine that we can define over it, and its universal property as having freely added comprehensions.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.