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.
