One ingredient in (the categorical comprehension situation), as considered by Lawvere, Street, Walters, et al is (the factorization of functors) in ( (a categorical version) of ( (the classic epi-mono factorization of functions) in (the category of sets) ) ).
That factorization, in $\Set$, uses the notion of image, which in turn uses the logical notion of existence: $(f : X \to Y) \, \leftadj{ \text{Image} } = \{ y\in Y | (\leftadj\exists x\in X)(xf=y) \}$.
Note how comprehension is used in the above definition.
A version of this can be produced in an arbitrary category, using certain standard categorical notions.
(When applied to $\Set$, one does not recover the subset of $Y$ defined above.)
The diagram below, an expansion of
(the general categorical definition in Theorem 3 of [Street-Walters 1973]),
shows how this is done.
Here $f : A \to B$ is in general a functor between categories.
But the best introduction to this result is to take $A$ and $B$ to be discrete, i.e. essentially just sets, and $f$ merely a set-theoretic function between them,
then to interpret the various constructs in that simple situation, i.e. in $\Set$.
Note (the result)
is NOT even isomorphic to
(the standard epic-monic factorization of $f$).
\[ \boxed{ \begin{array} {} & {} \rlap{ \kern-2em \rightadj{ \text{left fiber} } } \\ & \rightadj{ \llap{(2) \;} \boxed{(\black f \downarrow \black b)} } & \rightadj{ \xrightarrow [\smash{}] {\textstyle a} } & A \rlap{ \kern.5em \xrightarrow [\smash{\kern13.5em}] {\textstyle !_A} } &&&& \calI \rlap{ \kern0em \xrightarrow [\smash{\kern6em}] {\textstyle \ulcorner 1 \urcorner} } && & \Set \\ &&&& \leftcat{ \searrow \rlap{\kern-.1em e \; (5)} } && \rightadj\nearrow \\ & \smash{ \rightadj{\llap ! \Bigg\downarrow} } & \smash{ \rightadj{ \llap\beta \Bigg\Downarrow} } & \smash{ \llap f \Bigg\downarrow \rlap{ \kern0em \scriptstyle \red{ { \calE-\calM \atop \text{factorization} } } } } && \rightadj{ \boxed{(\black 1 \downarrow \leftadj k) \; (4)} } \rlap{ \kern0em \smash{ \leftadj{ \Bigg\Downarrow { \text{for the $\Lan$} \atop \textstyle \leftadj{\iota \; (3)} } } } } &&& \smash{ \rightadj{ \Bigg\Downarrow \rlap{ \kern-.25em { \text{for the} \atop \text{comma cat} } } } } & & \smash{\Bigg\Vert} \\ &&&& \rightadj{ \swarrow \rlap{\kern-.1em p} } \\ & \calI & \xrightarrow [\textstyle b \; (1)] {\smash{\kern3em}} & B \rlap{ \kern.5em \leftadj{ \xrightarrow [ \textstyle \boxed{ \textstyle \black{(!_A \ulcorner 1 \urcorner)} \Lan_{\black f} = k } \; (3) \; \text{(fiber colimit)} ] {\smash{\kern21em}} } } &&&&&& \kern1em & \Set \\ \kern1em &&&& {} \rlap{ \kern-1em B\text{-indexed} \leftadj{ \text{ family of left-fiber colimits} } } \\ \end{array} } \]
<hr />
-----------
An instructive, very concrete, example of this situation is:
\[ \boxed{ \begin{array} {} & {} \rlap{ \kern-4em \rightadj{ \text{left fiber (pullback)} } } \\ \text{e.g.:} & \rightadj{ \text{Mike}[\text{Mike}g=\text{M}] } & \mapsto & \text{Mike} && \mapsto && \star & \mapsto && 1 \\ & \rightadj{ \llap{(2) \;} \boxed{ \begin{array} {} (\black g \downarrow \black{ \text{M} }) \\ \text{Mike}[\text{Mike}g=\text{M}], \text{etc.} \\ \end{array} } } & \rightadj{ \xrightarrow [\smash{}] { \textstyle \text{names}_{ \black{\text{M}} } } } & \boxed{ \begin{array} {} \text{Names} \\ \text{Mike, Marty, Mo, Fran, Flo} \\ \end{array} } \rlap{ \kern.5em \xrightarrow [\smash{\kern24em}] { \textstyle !_{ \text{Names} } } } &&&& \calI \rlap{ \kern0em \xrightarrow [\smash{\kern6em}] {\textstyle \ulcorner 1 \urcorner} } && & \Set \\ &&&& \leftcat{ \searrow \rlap{\kern-.1em e \; (5)} } && \rightadj\nearrow \\ & \smash{ \rightadj{\llap ! \Bigg\downarrow} } & \smash{ \rightadj{\Bigg\Downarrow} } & \smash{ \llap g \Bigg\downarrow \rlap{ \kern1em \red{ { \calE-\calM \atop \text{factorization} } } } } && \rightadj{ \boxed{ \begin{array}{} (\black 1 \downarrow \leftadj k) \; (4) \\ \text{M}[0], \text{M}[1], \text{M}[2], \text{F}[0], \text{F}[1] \\ \end{array} } } \rlap{ \kern0em \smash{ \leftadj{ \Bigg\Downarrow { \text{for the $\Lan$} \atop \textstyle \leftadj{\iota \; (3)} } } } } &&& \smash{ \rightadj{ \Bigg\Downarrow \rlap{ \kern-.25em { \text{for the} \atop \text{comma cat} } } } } & & \smash{\Bigg\Vert} \\ &&&& \rightadj{ \swarrow \rlap{\kern-.2em p} } \\ & \calI \rlap{ \xrightarrow [\textstyle \text{M} \; (1)] { \smash{\kern20em} } } && \boxed{ \begin{array} {} \text{Genders} \\ \text{M, F, N} \\ \end{array} } \rlap{ \kern.5em \leftadj{ \xrightarrow [ \textstyle \boxed{ \textstyle \black{(!_{\text{Names}} \ulcorner 1 \urcorner)} \Lan_{\black g} = k } \; (3) \; \text{(fiber colimit)} ] {\smash{\kern37em}} } } &&&&&& \kern1em & \Set \\ &&& {} \rlap{ \leftadj{ \kern0em \black{\text{M}}k = \black 1 + \black 1 + \black 1 = 3 = \{0,1,2\} ; \; \black{\text{F}}k = \black 1 + \black 1 = 2 = \{0,1\} ; \; \black{\text{N}}k = \leftadj\emptyset } .} \\ \kern1em &&&& {} \rlap{ \kern-5em \text{Genders-indexed} \leftadj{ \text{ family of left-fiber colimits} } } \\ \end{array} } \]
The national transformation $\leftadj\iota$ of the $\leftadj\Lan$ deserve a closer look.
The key point is that
it is (the natural transformation $\leftadj\iota$) that links
each (individual name) with
( a specific element of (the sets that are colimits) that form (the image of the $\leftadj\Lan$ in $\Set$) ).
\[ \boxed{ \begin{array} {ccccccccc|cc} \kern1em & \rightadj{ \llap{(2) \;} \boxed{ \begin{array} {} (\black g \downarrow \black{ \text{M} }) \\ \text{Mike}[\text{Mike}g=\text{M}], \text{etc.} \\ \end{array} } } & \rightadj{ \xrightarrow [\smash{}] { \textstyle \text{names}_{ \black{\text{M}} } } } & \boxed{ \begin{array} {} \text{Names} \\ \text{Mike, Marty, Mo, Fran, Flo} \\ \end{array} } \rlap{ \kern.5em \xrightarrow [\smash{\kern6em}] { \textstyle !_{ \text{Names} } } } && \calI \rlap{ \kern0em \xrightarrow [\smash{\kern8em}] {\textstyle \ulcorner 1 \urcorner} } && & \Set & 1 & \kern3em \\ & & \smash{ \rightadj{\llap ! \searrow} } & \smash{ \rightadj{\bigg\Downarrow} } & \llap g \searrow & \smash{ \leftadj{\bigg\Downarrow \rlap\iota} } & \leftadj{ \nearrow \rlap{ \boxed{ \textstyle \black{(!_{\text{Names}} \ulcorner 1 \urcorner)} \Lan_{\black g} = k } \; (3) \; \text{(fiber colimit)} } } &&& \smash{ \leftadj{\Bigg\downarrow} \rlap{ \raise3ex { \leftadj\iota _{\text{Mike}} } } } \\ & && \calI \rlap{ \xrightarrow [\textstyle \text{M} \; (1)] { \smash{\kern12em} } } && \boxed{ \begin{array} {} \text{Genders} \\ \text{M, F, N} \\ \end{array} } &&&& \leftadj{ \black{\text{Mike}g}k = \black{\text{M}} k = 3 } \\ \end{array} } \]
Using the notation and setup of the above, we then have
\[ { \black{\text{Mike}} }e = (\black{\text{Mike}}g = \text{M}) \big[ \leftadj{ \iota_{\black{\text{Mike}}} : \black 1 \to \black{ (\text{Mike}g) } k = \black{\text{M}} k = 3 } \big] \]
<hr />
Very preliminary draft!! (A work in progress) :
Categorical Comprehension Schema:
Street-Walters:
The general case in Street-Walters requires the following:
Here
(${\bf T}$ is a (possibly large) category, of "types" or "contexts"),
($P : {\bf T}\op \to \Cat$ is a functor, a "hyperdoctrine"), and
($X\in {\bf T}$ is a "type" or "context").
\[ \boxed{ \begin{array} {} \leftcat{ ({\bf T}\downarrow X) } & \mathop\rightleftarrows\limits^{\leftadj\Omega}_{\rightadj\Theta} & \rightcat{ XP } & \rightcat{=} & \rightcat{ (\calM \downarrow X) } & \rightcat{\approx} & \rightcat{ \hom X {\bf T} \Omega } \\ \end{array} } \]
Examples:
\[ \boxed{ \begin{array} {ccc|ccccccc} {\bf T} & \ni & \Omega & \leftcat{ ({\bf T}\downarrow X) } & \mathop\rightleftarrows\limits^{\leftadj\Omega}_{\rightadj\Theta} & \rightcat{ XP } & \rightcat{=} & \rightcat{ (\calM \downarrow X) } & \rightcat{\approx} & \rightcat{ \hom X {\bf T} \Omega } \\ &&&&& \rightcat{ \text{attributes} } \\ \hline \Set & \ni & 2 & \leftcat{ (\Set\downarrow X) } & \mathop\rightleftarrows\limits^{\leftadj\Omega}_{\rightadj\Theta} & \rightcat{ XP } & \rightcat{=} & \rightcat{ ( \text{(monics)} \downarrow X) } & \rightcat{\approx} & \rightcat{ \hom X \Set 2} & \rightcat{=} & \rightcat{ [X,2] } \\ &&& \leftcat{ \text{oversets} } && \rightcat{ \text{attributes} } && \rightcat{ \text{monics} } && {} \rlap{ \rightcat{ \kern2em \text{predicates} } } \\ \hline \Set & & \Set & \leftcat{ (\Set \downarrow X) } & \mathop\rightleftarrows\limits^{\leftadj\Omega}_{\rightadj\Theta} & \rightcat{ XP } & \rightcat{=} & \rightcat{ (\text{(dofs)} \downarrow X) } & \rightcat{\approx} & \rightcat{ \hom X \SET \Set} & \rightcat{=} & \rightcat{ [X,\Set] } \\ &&& \leftcat{ \text{oversets} } && \rightcat{ \text{attributes} } && {} \rlap{ \kern-4em \rightcat{ \text{} } } && {} \rlap{ \rightcat{ \kern2em \text{indexed families} } } \\ \hline \CAT & \ni & \Set & \leftcat{ (\CAT \downarrow X) } & \mathop\rightleftarrows\limits^{\leftadj\Omega}_{\rightadj\Theta} & \rightcat{ XP } & \rightcat{=} & \rightcat{ ( \text{(dofs) } \downarrow X) } & \rightcat{\approx} & \rightcat{ \hom X \CAT \Set} & \rightcat{=} & \rightcat{ [X,\Set] } \\ &&& \leftcat{ \text{overcategories} } && \rightcat{ \text{attributes} } && {} \rlap{ \kern-4em \rightcat{ \text{discrete op-fibrations (dofs)} } } && {} \rlap{ \rightcat{ \kern2em \text{indexed families} } } \\ \end{array} } \]
References:
https://ncatlab.org/nlab/show/hyperdoctrine
https://ncatlab.org/nlab/show/axiom+of+separation
\boxed{ \begin{array} {} \text{ } \\ \text{ } \\ \end{array} }
\[ 3 = 1+1+1 = {0} + {0} + {0} = {0,1,2} = [2] \]
