Adjunctions, Limits, and Locally Cartesian Closure

Proof. For (1), ${\mathrm{id}}_{a\times b}$ satisfies the two equations (142.2) required of $⟨{\mathsf{pr}}_1,{\mathsf{pr}}_2⟩$, because ${\mathsf{pr}}_i\circ {\mathrm{id}}_{a\times b}={\mathsf{pr}}_i$ by the unit law; the uniqueness clause of definition 142.1 applied to the pair $({\mathsf{pr}}_1,{\mathsf{pr}}_2)$ then identifies the two arrows.

For (2), the arrow $⟨f,g⟩\circ h$ satisfies the two equations required of $⟨f\circ h,g\circ h⟩$: $${\mathsf{pr}}_1\circ (⟨f,g⟩\circ h)\stackrel{assoc.}{=}({\mathsf{pr}}_1\circ ⟨f,g⟩)\circ h\stackrel{(142.2)}{=}f\circ h,$$ and the same calculation with ${\mathsf{pr}}_2$ and $g$. Uniqueness applied to the pair $(f\circ h,g\circ h)$ gives the equation. ◻

Proof. Existence and uniqueness of $u$ are the universal property of $p^{\prime }$ applied to the pair $({\mathsf{pr}}_1,{\mathsf{pr}}_2)$ out of $p$. Symmetrically there is exactly one $v:p^{\prime }⟶p$ with ${\mathsf{pr}}_i\circ v={\mathsf{pr}}_i^{\prime }$. Then $${\mathsf{pr}}_i\circ (v\circ u)\stackrel{assoc.}{=}({\mathsf{pr}}_i\circ v)\circ u\stackrel{def.v}{=}{\mathsf{pr}}_i^{\prime }\circ u\stackrel{def.u}{=}{\mathsf{pr}}_i\stackrel{unit}{=}{\mathsf{pr}}_i\circ {\mathrm{id}}_p,$$ for $i=1,2$, so $v\circ u$ and ${\mathrm{id}}_p$ both mediate the pair $({\mathsf{pr}}_1,{\mathsf{pr}}_2)$; uniqueness in the universal property of $p$ gives $v\circ u={\mathrm{id}}_p$. Exchanging the roles of $p$ and $p^{\prime }$ gives $u\circ v={\mathrm{id}}_{p^{\prime }}$. ◻

Proof. Each $x_i$ has type $A_i$ in $\mathrm{\Gamma }\mathrm{\Delta }$ by Var, and likewise each $y_j$, so both lists are substitutions in the sense of definition 141.1. Let $f=(a_1,\dots ,a_n):\mathrm{\Xi }⟶\mathrm{\Gamma }$ and $g=(b_1,\dots ,b_m):\mathrm{\Xi }⟶\mathrm{\Delta }$. The concatenated list $$⟨f,g⟩:=(a_1,\dots ,a_n,b_1,\dots ,b_m)$$ is a substitution $\mathrm{\Xi }⟶\mathrm{\Gamma }\mathrm{\Delta }$, since its $i$-th entry has the type declared at position $i$ of $\mathrm{\Gamma }\mathrm{\Delta }$. Composition acts entrywise by definition 141.4, so $${\mathsf{pr}}_1\circ ⟨f,g⟩=(x_1[⟨f,g⟩],\dots ,x_n[⟨f,g⟩])=(a_1,\dots ,a_n)=f,$$ and the same calculation gives ${\mathsf{pr}}_2\circ ⟨f,g⟩=g$. For uniqueness, let $h=(c_1,\dots ,c_{n+m})$ satisfy the two equations. Its composite with ${\mathsf{pr}}_1$ is $(c_1,\dots ,c_n)$, so $c_i=a_i$ for $i\le n$; its composite with ${\mathsf{pr}}_2$ is $(c_{n+1},\dots ,c_{n+m})$, so $c_{n+j}=b_j$. Hence $h=⟨f,g⟩$.

For the empty context, a substitution $\mathrm{\Xi }⟶$ is the empty list, and there is exactly one empty list. ◻

Proof. Commutation. For $(d,e)\in \mathrm{\Delta }{\times }_{\mathrm{\Gamma }}E$ the defining condition gives $\gamma (u(d,e))=\gamma (d)=p(e)=p(v(d,e))$.

Existence. Let $u^{\prime }:X\to \mathrm{\Delta }$ and $v^{\prime }:X\to E$ satisfy $\gamma \circ u^{\prime }=p\circ v^{\prime }$. For $x\in X$ the pair $(u^{\prime }(x),v^{\prime }(x))$ satisfies $\gamma (u^{\prime }(x))=p(v^{\prime }(x))$, hence lies in $\mathrm{\Delta }{\times }_{\mathrm{\Gamma }}E$. Put $h(x):=(u^{\prime }(x),v^{\prime }(x))$; then $u\circ h=u^{\prime }$ and $v\circ h=v^{\prime }$ by the definition of $u$ and $v$.

Uniqueness. If $h^{\prime }$ also satisfies the two equations then for each $x$ the pair $h^{\prime }(x)$ has first component $u^{\prime }(x)$ and second component $v^{\prime }(x)$, so $h^{\prime }(x)=h(x)$.

Fibers. Fix $d\in \mathrm{\Delta }$. The map $e\mapsto (d,e)$ sends $p^{-1}(\gamma (d))$ into $u^{-1}(d)$, and $(d,e)\mapsto e$ sends $u^{-1}(d)$ into $p^{-1}(\gamma (d))$; the two are mutually inverse. ◻

Proof. Write $f=(a_1,\dots ,a_n)$.

Well-formedness. From $\mathrm{\Gamma }⊢A\mathsf{type}$ and $f$ the action of proposition 71.51 gives $\mathrm{\Delta }⊢A[f]\mathsf{type}$, so $\mathrm{\Delta }.A[f]$ is a context. The list $f^{+}$ has entries $a_1[w_{A[f]}],\dots ,a_n[w_{A[f]}]$ followed by $x$. The first $n$ entries have the types of $\mathrm{\Gamma }$ by weakening, and the last has type $$A[f\circ w_{A[f]}]\stackrel{proposition71.51}{=}A[f][w_{A[f]}],$$ which is the type required at the last declaration of $\mathrm{\Gamma }.A$.

Commutation. Both composites are the list $(a_1[w_{A[f]}],\dots ,a_n[w_{A[f]}])$: on one side because $w_A$ selects the first $n$ entries of $f^{+}$, on the other by entrywise substitution.

Existence. Let $h:\mathrm{\Xi }⟶\mathrm{\Delta }$ and $k:\mathrm{\Xi }⟶\mathrm{\Gamma }.A$ satisfy $f\circ h=w_A\circ k$. Split $k=(k_0,c)$ where $k_0$ is the list of its first $n$ entries and $\mathrm{\Xi }⊢c:A[k_0]$. Then $w_A\circ k=k_0$, so the hypothesis reads $k_0=f\circ h$, whence $$A[k_0]=A[f\circ h]\stackrel{proposition71.51}{=}A[f][h],$$ and $\mathrm{\Xi }⊢c:A[f][h]$. Therefore $m:=(h,c)$ is a context substitution $\mathrm{\Xi }⟶\mathrm{\Delta }.A[f]$. It satisfies $w_{A[f]}\circ m=h$, since $w_{A[f]}$ selects the first entries; and $$f^{+}\circ m=(a_1[w_{A[f]}][m],\dots ,a_n[w_{A[f]}][m],x[m])=(f\circ h,c)=(k_0,c)=k.$$

Uniqueness. Let $m^{\prime }$ satisfy the same two equations. From $w_{A[f]}\circ m^{\prime }=h$ its first entries are judgmentally equal to those of $h$, and from $f^{+}\circ m^{\prime }=k$ its last entry is judgmentally equal to $c$. Hence $m^{\prime }=m$ as an arrow of ${\mathbf{Ctx}}_{\mathcal{T}}$. ◻

Proof. Terminal objects and binary products give a product $\prod _{i}D(i)$ of the finitely many objects $D(i)$, by induction on their number: the empty product is the terminal object and $\prod _{i\le n+1}=(\prod _{i\le n})\times D(n+1)$; write ${\rho }_i$ for the resulting projections. Likewise form $\prod _{\alpha }D(\mathrm{tgt}\alpha )$ over the finitely many arrows $\alpha$ of $\mathcal{J}$, with projections ${\rho }_{\alpha }$. Define $u,v:\prod _{i}D(i)⟶\prod _{\alpha }D(\mathrm{tgt}\alpha )$ as the unique arrows with $${\rho }_{\alpha }\circ u=D(\alpha )\circ {\rho }_{\mathrm{src}\alpha },{\rho }_{\alpha }\circ v={\rho }_{\mathrm{tgt}\alpha }$$ for every $\alpha$; these exist and are unique by the universal property of the second product. Let $i:e⟶\prod _{i}D(i)$ be an equalizer of $u$ and $v$, and put ${\pi }_i:={\rho }_i\circ i$.

$(e,({\pi }_i))$ is a cone. For $\alpha :i⟶j$, $$D(\alpha )\circ {\pi }_i\stackrel{def.}{=}D(\alpha )\circ {\rho }_i\circ i\stackrel{def.u}{=}{\rho }_{\alpha }\circ u\circ i\stackrel{equalizer}{=}{\rho }_{\alpha }\circ v\circ i\stackrel{def.v}{=}{\rho }_j\circ i\stackrel{def.}{=}{\pi }_j.$$

Universality. Let $(c,({\tau }_i))$ be a cone. Let $t:c⟶\prod _{i}D(i)$ be the unique arrow with ${\rho }_i\circ t={\tau }_i$. Then for each $\alpha :i⟶j$, $${\rho }_{\alpha }\circ u\circ t\stackrel{def.u}{=}D(\alpha )\circ {\rho }_i\circ t\stackrel{def.t}{=}D(\alpha )\circ {\tau }_i\stackrel{cone}{=}{\tau }_j\stackrel{def.t}{=}{\rho }_j\circ t\stackrel{def.v}{=}{\rho }_{\alpha }\circ v\circ t,$$ and since this holds for every $\alpha$, uniqueness in the universal property of $\prod _{\alpha }$ gives $u\circ t=v\circ t$. Hence $t=i\circ h$ for exactly one $h:c⟶e$, and ${\pi }_i\circ h={\rho }_i\circ i\circ h={\rho }_i\circ t={\tau }_i$. If $h^{\prime }$ also satisfies ${\pi }_i\circ h^{\prime }={\tau }_i$ for all $i$, then $i\circ h^{\prime }$ and $i\circ h$ have the same composites with every ${\rho }_i$, so $i\circ h^{\prime }=t=i\circ h$, and uniqueness of the equalizer factorization gives $h^{\prime }=h$. ◻

Proof. The stated diagram is the case of theorem 142.15 in which $\mathcal{J}$ has objects $1,2,3$ and two nonidentity arrows $1\to 3\leftarrow 2$; the product over the objects is $\mathrm{\Delta }\times E\times \mathrm{\Gamma }$ and the equalizer conditions reduce to $\gamma \circ {\mathsf{pr}}_1=p\circ {\mathsf{pr}}_2$ after deleting the redundant third factor, since the cone component at $3$ is determined by the component at $1$. ◻

Proof. $F$ is a functor. Acting entrywise preserves concatenation and the empty list, so $Fh$ is a homomorphism; entrywise action of a composite is the composite of entrywise actions, and entrywise action of the identity is the identity.

$\phi$ is a bijection. The paragraph opening this section showed that for each $k:S\to UM$ there is exactly one homomorphism $\hat{k}$ with $U\hat{k}\circ {\eta }_S=k$, which is exactly the statement that $\phi$ is injective and surjective.

First equation. Let $h:S^{\prime }\to S$ and $\hat{k}:S^{\ast }⟶M$. Both sides are functions $S^{\prime }\to UM$; evaluate at $s^{\prime }\in S^{\prime }$: $$\phi (\hat{k}\circ Fh)(s^{\prime })\stackrel{def.\phi }{=}\hat{k}(Fh([s^{\prime }]))\stackrel{entrywise}{=}\hat{k}([h(s^{\prime })])\stackrel{def.\phi }{=}\phi (\hat{k})(h(s^{\prime })).$$

Second equation. Let $l:M⟶M^{\prime }$ be a homomorphism. At $s\in S$, $$\phi (l\circ \hat{k})(s)\stackrel{def.\phi }{=}l(\hat{k}([s]))\stackrel{def.\phi }{=}Ul(\phi (\hat{k})(s)),$$ which is the value of $Ul\circ \phi (\hat{k})$ at $s$. ◻

Proof. The proof uses only the two equations (142.5) and the functor laws; every step is one of them.

(1) Naturality of $\eta$. Let $h:c^{\prime }⟶c$. Then $$GFh\circ {\eta }_{c^{\prime }}\stackrel{(142.5)(2)}{=}\phi (Fh\circ {\mathrm{id}}_{F{c}^{\prime }})\stackrel{unit}{=}\phi (Fh)\stackrel{unit}{=}\phi ({\mathrm{id}}_{Fc}\circ Fh)\stackrel{(142.5)(1)}{=}{\eta }_c\circ h.$$ Naturality of $\epsilon$ is the same calculation performed on ${\phi }^{-1}$, whose two equations are obtained from (142.5) by applying ${\phi }^{-1}$ to both sides: ${\phi }^{-1}(f\circ h)={\phi }^{-1}(f)\circ Fh$ and ${\phi }^{-1}(Gk\circ f)=k\circ {\phi }^{-1}(f)$. Explicitly, for $l:d⟶d^{\prime }$, $${\epsilon }_{d^{\prime }}\circ FGl\stackrel{{\phi }^{-1}(1)}{=}{\phi }^{-1}({\mathrm{id}}_{G{d}^{\prime }}\circ Gl)\stackrel{unit}{=}{\phi }^{-1}(Gl)\stackrel{unit}{=}{\phi }^{-1}(Gl\circ {\mathrm{id}}_{Gd})\stackrel{{\phi }^{-1}(2)}{=}l\circ {\epsilon }_d.$$

(1) Triangle identities. For the first, $$\phi ({\epsilon }_{Fc}\circ F{\eta }_c)\stackrel{(142.5)(1)}{=}\phi ({\epsilon }_{Fc})\circ {\eta }_c\stackrel{def.\epsilon }{=}{\mathrm{id}}_{GFc}\circ {\eta }_c\stackrel{unit}{=}{\eta }_c\stackrel{def.\eta }{=}\phi ({\mathrm{id}}_{Fc}),$$ and $\phi$ is injective, so ${\epsilon }_{Fc}\circ F{\eta }_c={\mathrm{id}}_{Fc}$. For the second, apply ${\phi }^{-1}$ to $G{\epsilon }_d\circ {\eta }_{Gd}$: $${\phi }^{-1}(G{\epsilon }_d\circ {\eta }_{Gd})\stackrel{{\phi }^{-1}(2)}{=}{\epsilon }_d\circ {\phi }^{-1}({\eta }_{Gd})\stackrel{def.\eta }{=}{\epsilon }_d\circ {\mathrm{id}}_{FGd}\stackrel{unit}{=}{\epsilon }_d\stackrel{def.\epsilon }{=}{\phi }^{-1}({\mathrm{id}}_{Gd}).$$

(2) $\phi$ and $\psi$ are mutually inverse. For $g:Fc⟶d$, $$\psi (\phi (g))\stackrel{def.}{=}{\epsilon }_d\circ F(Gg\circ {\eta }_c)\stackrel{functor}{=}{\epsilon }_d\circ FGg\circ F{\eta }_c\stackrel{\epsilon natural}{=}g\circ {\epsilon }_{Fc}\circ F{\eta }_c\stackrel{(142.6)(1)}{=}g.$$ For $f:c⟶Gd$, $$\phi (\psi (f))\stackrel{def.}{=}G({\epsilon }_d\circ Ff)\circ {\eta }_c\stackrel{functor}{=}G{\epsilon }_d\circ GFf\circ {\eta }_c\stackrel{\eta natural}{=}G{\epsilon }_d\circ {\eta }_{Gd}\circ f\stackrel{(142.6)(2)}{=}f.$$

(2) The two equations. For $h:c^{\prime }⟶c$, $$\phi (g\circ Fh)\stackrel{def.}{=}G(g\circ Fh)\circ {\eta }_{c^{\prime }}\stackrel{functor}{=}Gg\circ GFh\circ {\eta }_{c^{\prime }}\stackrel{\eta natural}{=}Gg\circ {\eta }_c\circ h\stackrel{def.}{=}\phi (g)\circ h,$$ and for $k:d⟶d^{\prime }$, $$\phi (k\circ g)\stackrel{def.}{=}G(k\circ g)\circ {\eta }_c\stackrel{functor}{=}Gk\circ Gg\circ {\eta }_c\stackrel{def.}{=}Gk\circ \phi (g).$$

(3). Starting from $\phi$, part (1) produces ${\eta }_c=\phi ({\mathrm{id}}_{Fc})$, and part (2) then rebuilds $g\mapsto Gg\circ \phi ({\mathrm{id}}_{Fc})=\phi (g\circ {\mathrm{id}}_{Fc})=\phi (g)$ by (142.5)(2) and the unit law. Starting from $(\eta ,\epsilon )$, part (2) produces $\phi$, and part (1) returns $\phi ({\mathrm{id}}_{Fc})=G{\mathrm{id}}_{Fc}\circ {\eta }_c={\eta }_c$ and $\psi ({\mathrm{id}}_{Gd})={\epsilon }_d\circ F{\mathrm{id}}_{Gd}={\epsilon }_d$. ◻