局所デカルト閉圏

射 $g\colon A\times F\to E$ の転置を $\tilde g\colon A\to E^F$ と書く。転置の $E$ についての自然性から、$p\circ g$ の転置は $p^F\circ\tilde g$ である。$A$ についての自然性から、射影 $\mathrm{pr}_2\colon A\times F\to F$（$=\mathrm{pr}_2\circ(!_A\times\mathrm{id}_F)$、$!_A\colon A\to1$）の転置は $\ulcorner\mathrm{id}\urcorner\circ!_A$ である。転置は全単射なので
$$ p\circ g=\mathrm{pr}_2\iff p^F\circ\tilde g=\ulcorner\mathrm{id}\urcorner\circ!_A $$
であり、右辺は $\tilde g$ が引き戻し $\Gamma_F(p)\to E^F$ をただ 1 通りに経由することと同値である。左辺は $g$ が $\mathcal D/F$ の射 $(A\times F,\mathrm{pr}_2)\to(E,p)$ であることにほかならない。よって
$$ \operatorname{Hom}_{\mathcal D/F}\bigl((A\times F,\mathrm{pr}_2),(E,p)\bigr)\cong\operatorname{Hom}_{\mathcal D}\bigl(A,\Gamma_F(p)\bigr) $$
であり、この全単射は、転置と引き戻しの普遍性がともに自然であることから $A$ について自然である。各 $p$ で $\operatorname{Hom}((-)\times F,p)$ が表現されたので、$\Gamma_F$ は射の上でも一意に関手に延び、全単射は $p$ についても自然になる（随伴関手）。$\square$

1 ⇒ 2。$f\colon Y\to X$ をとり、$\mathcal D:=\mathcal C/X$、$F:=(Y,f)$ とおく。仮定より $\mathcal D$ は Cartesian 閉である。rem-lccc-slice-of-slice の同型 $\Phi\colon\mathcal D/F\cong\mathcal C/Y$ で $(-)\times F\colon\mathcal D\to\mathcal D/F$ を写すと、$(B,b)$ は、$\mathcal D$ での積 $(B,b)\times(Y,f)$、すなわち $B\times_XY$ に $Y$ への射影を付けたものに移る。これは $f^*(B,b)$ と自然に同型である（どちらも同じ図式の引き戻しなので、引き戻しの普遍性による同型が自然に定まる）。lem-lccc-sections により $(-)\times F$ は右随伴 $\Gamma_F$ をもつので、$f^*$ は右随伴 $\Pi_f:=\Gamma_F\circ\Phi^{-1}$ をもつ（自然に同型な関手は同じ右随伴をもつ）。
2 ⇒ 1。$X$ を対象とする。$\mathcal C/X$ は終対象 $(X,\mathrm{id}_X)$ と積をもつ。対象 $(B,b)$ を固定すると、$(A,a)\mapsto(A,a)\times(B,b)$ は、$b^*(A,a)=(B\times_XA,\mathrm{pr}_1)$ に $\Sigma_b$ を施したもの $(B\times_XA,\ b\circ\mathrm{pr}_1)$ と自然に同型である。すなわち $(-)\times(B,b)\cong\Sigma_b\circ b^*$ である。$\Sigma_b\dashv b^*$ と $b^*\dashv\Pi_b$ を合成すると、$\Sigma_b\circ b^*$ は右随伴 $\Pi_b\circ b^*$ をもつ。よって $\mathcal C/X$ は Cartesian 閉で、指数対象は $\Pi_b\,b^*(A,a)$ である。$\square$

この圏で $x\to z\leftarrow y$ の引き戻しは $x\wedge y$ であり、スライス圏 $H/x$ は下集合 ${\downarrow}x=\{c\mid c\le x\}$ である。${\downarrow}x$ の終対象は $x$、積は $\wedge$ である。$a,b\le x$ に対し $(a\Rightarrow b)\wedge x\in{\downarrow}x$ とおくと、$c\le x$ について
$$ c\wedge a\le b\iff c\le a\Rightarrow b\iff c\le(a\Rightarrow b)\wedge x $$
なので、これが ${\downarrow}x$ での指数対象である。よって $H$ は局所デカルト閉である。$y\le x$ に沿った引き戻しは $b\mapsto b\wedge y$ であり、$a\le y$、$c\le x$ について $c\wedge y\le a\iff c\le y\Rightarrow a\iff c\le(y\Rightarrow a)\wedge x$ だから、右随伴は上の式で与えられる。$\square$

1。$\iota_i\colon A_i\to A$ を余極限の入射とし、$A_i$ に射 $a\circ\iota_i$ を付けて $\mathcal C/X$ の図式とみる。$(A,a)$ はその $\mathcal C/X$ での余極限である。実際、$\mathcal C/X$ の余錐 $h_i\colon(A_i,a\circ\iota_i)\to(W,w)$ が $\mathcal C$ で誘導する $u\colon A\to W$ は、各 $i$ で $w\circ u\circ\iota_i=w\circ h_i=a\circ\iota_i$ をみたすので、余極限の普遍性の一意性により $w\circ u=a$ であり、$\mathcal C/X$ の射である。
$g^*$ は右随伴 $\Pi_g$ をもつ（thm-lccc-pi）ので余極限を保ち、$(Z\times_XA,\mathrm{pr}_1)$ は $(Z\times_XA_i,\mathrm{pr}_1)$ の $\mathcal C/Z$ での余極限である。これが $\mathcal C$ での余極限でもあることを示す。$\mathcal C$ は終対象と引き戻しをもつので積をもつ。$\mathcal C$ の余錐 $c_i\colon Z\times_XA_i\to W$ が与えられたとき、$(c_i,\mathrm{pr}_1)\colon Z\times_XA_i\to W\times Z$ は $\mathcal C/Z$ の対象 $(W\times Z,\mathrm{pr}_2)$ への余錐なので、$Z$ 上の射 $v\colon Z\times_XA\to W\times Z$ がただ 1 つ誘導され、$u:=\mathrm{pr}_1\circ v$ が求める射である。$u'$ も同じ条件をみたせば、$(u',\mathrm{pr}_1)$ も同じ余錐を誘導する $Z$ 上の射なので $v$ に等しく、$u'=u$ である。
2。$\mathcal C/0$ では $(0,\mathrm{id}_0)$ が始対象かつ終対象である（$(B,b)$ に対し射 $0\to B$ はただ 1 つで、$b$ と合成すると $\mathrm{id}_0$ になる）。$k^*\colon\mathcal C/0\to\mathcal C/A$ は左随伴 $\Sigma_k$ と右随伴 $\Pi_k$ をもつので、終対象と始対象をともに保つ。よって $k^*(0,\mathrm{id}_0)$ は $\mathcal C/A$ の終対象 $(A,\mathrm{id}_A)$ とも始対象 $(0,\,0\to A)$ とも同型であり、$A\cong0$ である。$A$ は始対象なので $A$ から $0$ への射はただ 1 つであり、$k$ はこの同型に一致する。$\square$

$\mathcal C$ は終対象と引き戻しをもつので有限極限をもち、核対の余等化子は仮定により存在する。残るのは、正則エピ射が引き戻しで安定であることである。$e\colon A\to B$ を射 $u,v\colon R\to A$ の余等化子とし、$g\colon C\to B$ を任意の射とする。$e\circ u=e\circ v$ なので、$u,v$ は $\mathcal C/B$ の射 $(R,e\circ u)\to(A,e)$ とみなせる。
$e\colon(A,e)\to(B,\mathrm{id}_B)$ は $\mathcal C/B$ で $u,v$ の余等化子である。実際、$\mathcal C/B$ の射 $h\colon(A,e)\to(W,w)$ が $h\circ u=h\circ v$ をみたせば、$\mathcal C$ で $h=k\circ e$ となる $k\colon B\to W$ がただ 1 つあり、$w\circ k\circ e=w\circ h=e$ と、余等化子 $e$ がエピ射であることから $w\circ k=\mathrm{id}_B$ となる。
$g^*$ は左随伴なので、この余等化子を $\mathcal C/C$ の余等化子に写す。$g^*(B,\mathrm{id}_B)$ は $(C,\mathrm{id}_C)$ と同型だから、引き戻し $C\times_BA\to C$ は $\mathcal C/C$ で $g^*u,g^*v$ の余等化子であり、prop-lccc-colimits の 1 の証明の後半と同じ議論（積 $W\times C$ を使う）により $\mathcal C$ でも余等化子である。よって正則エピ射である。$\square$