ch:categories: ch:categories

With $\mathrm{\Theta }=z:\mathbf{2}\to \mathbf{2}$ and $\rho =(z\mathsf{ff})$, $$\rho \circ \tau =((z\mathsf{ff})[\tau ])=((\lambda w:\mathbf{2}.y)\mathsf{ff}):\mathrm{\Delta }⟶\mathrm{\Lambda },$$ so $(\rho \circ \tau )\circ \sigma =(((\lambda w:\mathbf{2}.y)\mathsf{ff})[(fx)/y])=((\lambda w:\mathbf{2}.fx)\mathsf{ff})$, the bound $w$ needing no change because $w$ is not free in $fx$. On the other side, $\tau \circ \sigma =(\lambda w:\mathbf{2}.fx)$ by the calculation in the text, and $\rho \circ (\tau \circ \sigma )=((z\mathsf{ff})[(\lambda w:\mathbf{2}.fx)/z])=((\lambda w:\mathbf{2}.fx)\mathsf{ff})$. The two lists coincide, as proposition 141.7 requires.

By the definition of composition in example 141.19, $$(x,x^{\prime })\in R^{⌣}\circ R⟺\mathrm{\exists }y.(x,y)\in R\wedge (x^{\prime },y)\in R,(y,y^{\prime })\in R\circ R^{⌣}⟺\mathrm{\exists }x.(x,y)\in R\wedge (x,y^{\prime })\in R.$$ Hence ${\mathrm{id}}_A\subseteq R^{⌣}\circ R$ says $\mathrm{\forall }x\in A.\mathrm{\exists }y.(x,y)\in R$, which is totality, and $R\circ R^{⌣}\subseteq {\mathrm{id}}_B$ says $(x,y)\in R\wedge (x,y^{\prime })\in R\Rightarrow y=y^{\prime }$, which is single-valuedness. A relation is the graph of a function exactly when it is total and single-valued: the function sends $x$ to the unique $y$ with $(x,y)\in R$.

First the claim in the hint. By the clauses of definition 2.41, $(e_1{e}_2)[\sigma ]$ is an application, $(\lambda y:B.b)[\sigma ]$ is an abstraction, and $\mathsf{tt}[\sigma ]=\mathsf{tt}$, $\mathsf{ff}[\sigma ]=\mathsf{ff}$; so if $t[\sigma ]$ is a variable then $t$ is a variable $x_i$ and $t[\sigma ]=\sigma (x_i)$.

Let $\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }$ and $\tau :\mathrm{\Delta }⟶\mathrm{\Gamma }$ with $\tau \circ \sigma ={\mathrm{id}}_{\mathrm{\Gamma }}$ and $\sigma \circ \tau ={\mathrm{id}}_{\mathrm{\Delta }}$. The first equation says $\tau (x_i)[\sigma ]=x_i$ for each declaration $x_i:A_i$ of $\mathrm{\Gamma }$; by the claim, $\tau (x_i)$ is a variable $y_{k(i)}$ of $\mathrm{\Delta }$ with $\sigma (y_{k(i)})=x_i$. Symmetrically the second equation gives, for each $y_j:B_j$ of $\mathrm{\Delta }$, a variable $x_{m(j)}$ with $\sigma (y_j)=x_{m(j)}$ and $\tau (x_{m(j)})=y_j$. Then $m(k(i))=i$ and $k(m(j))=j$, so $k$ and $m$ are mutually inverse bijections between the declarations of $\mathrm{\Gamma }$ and of $\mathrm{\Delta }$. Typing of the components gives $\mathrm{\Delta }⊢y_{k(i)}:A_i$, so $B_{k(i)}=A_i$. Thus $\mathrm{\Delta }$ lists the same types as $\mathrm{\Gamma }$, in the order given by $k$, under the renaming $x_i\mapsto y_{k(i)}$.

Conversely, if $\mathrm{\Delta }$ is obtained from $\mathrm{\Gamma }$ by a bijection $k$ on positions with $B_{k(i)}=A_i$ and a renaming, then $\sigma :=(x_{m(1)},\dots ,x_{m(|\mathrm{\Delta }|)})$ and $\tau :=(y_{k(1)},\dots ,y_{k(|\mathrm{\Gamma }|)})$ are substitutions, and $(\tau \circ \sigma )(x_i)=y_{k(i)}[\sigma ]=x_{m(k(i))}=x_i$, likewise for the other composite.

Let $0$ and $0^{\prime }$ be initial and let $i:0⟶0^{\prime }$ and $i^{\prime }:0^{\prime }⟶0$ be the unique arrows. Then $i^{\prime }\circ i:0⟶0$ and ${\mathrm{id}}_0$ are both arrows $0⟶0$, so they are equal by uniqueness; likewise $i\circ i^{\prime }={\mathrm{id}}_{0^{\prime }}$. Any isomorphism $0⟶0^{\prime }$ is an arrow $0⟶0^{\prime }$, hence equals $i$. Compared with the displayed proof, every arrow has been reversed: $t:1⟶1^{\prime }$ became $i:0⟶0^{\prime }$ with the source and target exchanged, and the composite $t^{\prime }\circ t:1⟶1$ became $i^{\prime }\circ i:0⟶0$, which is the reversed composite $t{\circ }^{\mathrm{op}}{t}^{\prime }$ read in ${\mathcal{C}}^{\mathrm{op}}$.

Let $r\circ f={\mathrm{id}}_a$. If $f\circ u=f\circ u^{\prime }$ for $u,u^{\prime }:t⟶a$, then $$u\stackrel{unit}{=}{\mathrm{id}}_a\circ u=(r\circ f)\circ u\stackrel{assoc.}{=}r\circ (f\circ u)\stackrel{hyp.}{=}r\circ (f\circ u^{\prime })\stackrel{assoc.}{=}(r\circ f)\circ u^{\prime }=u^{\prime },$$ so $f$ is monic. If moreover $f$ is epic, compute $(f\circ r)\circ f\stackrel{assoc.}{=}f\circ (r\circ f)=f\circ {\mathrm{id}}_a=f={\mathrm{id}}_b\circ f$; cancelling the epimorphism $f$ on the right gives $f\circ r={\mathrm{id}}_b$. Together with $r\circ f={\mathrm{id}}_a$ this makes $f$ an isomorphism with inverse $r$.

If $g\circ f={\mathrm{id}}_a$ and $f\circ g={\mathrm{id}}_b$, then $$F(g)\circ F(f)\stackrel{(141.4)}{=}F(g\circ f)\stackrel{hyp.}{=}F({\mathrm{id}}_a)\stackrel{(141.4)}{=}{\mathrm{id}}_{F(a)},$$ and likewise $F(f)\circ F(g)={\mathrm{id}}_{F(b)}$; so $F(f)$ is an isomorphism and, by lemma 141.22, $F(f{)}^{-1}=F(g)=F(f^{-1})$.

For the converse, let $P=\{a,b\}$ with $a\le b$ and not $b\le a$, let $Q$ be the one-element preorder $\{\ast \}$, and let $F$ send both objects to $\ast$; $F$ is monotone, hence a functor by example 141.33. The arrow $f$ given by $a\le b$ is sent to ${\mathrm{id}}_{\ast }$, an isomorphism, but $f$ is not an isomorphism in $P$, because an inverse would be an arrow $b⟶a$ and ${\mathrm{hom}}_P(b,a)$ is empty.

For $f:a⟶b$, $g:b⟶c$ in $\mathcal{C}$ and $(u,u^{\prime })\in (K\times K^{\prime })(c)$, $$(K\times K^{\prime })(g\circ f)(u,u^{\prime })=(K(g\circ f)(u),K^{\prime }(g\circ f)(u^{\prime }))\stackrel{(141.5)}{=}(K(f)(K(g)(u)),K^{\prime }(f)(K^{\prime }(g)(u^{\prime })))=(K\times K^{\prime })(f)((K\times K^{\prime })(g)(u,u^{\prime })),$$ and $(K\times K^{\prime })({\mathrm{id}}_a)(u,u^{\prime })=(u,u^{\prime })$ by the identity clause of (141.5) in each component. For the conditional: if $\mathrm{\Gamma }⊢e:\mathbf{2}$ and $\mathrm{\Gamma }⊢e_i:A$ then $\mathrm{\Gamma }⊢\mathsf{if}(e;e_1;e_2):A$ by the conditional rule of chapter 2, so the map is well defined, and the nonbinding-constructor clause of definition 2.41, which recurses in the immediate subterms, gives, for every $\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }$, $$\mathsf{if}(e;e_1;e_2)[\sigma ]=\mathsf{if}(e[\sigma ];e_1[\sigma ];e_2[\sigma ]),$$ the analogue of (141.6).

Naturality of $\mathrm{at}$ at $\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }$ requires, for $e\in {\mathrm{Tm}}_{A\to B}(\mathrm{\Delta })$, $(et)[\sigma ]=e[\sigma ]t$. By the application clause the left side is $e[\sigma ]t[\sigma ]$, so the requirement is $t[\sigma ]=t$, which is lemma 141.2(3) because $t$ is closed. The one property used is $\mathrm{FV}(t)=\mathrm{\varnothing }$; for an open $t$ the family is not natural in general, because $t[\sigma ]$ can differ from $t$.

Choose $x^{\prime }\ne x$ and let ${\mathrm{\Delta }}_2:=(x:A,x^{\prime }:A^{\prime })$. By proposition 141.62 with $\mathrm{\Gamma }=⟨A⟩$, $\mathrm{y}({\mathrm{\Delta }}_2)\cong \mathrm{y}(⟨A⟩)\times {\mathrm{Tm}}_{A^{\prime }}$, and by proposition 141.60, $\mathrm{y}(⟨A⟩)\cong {\mathrm{Tm}}_A$; composing the natural isomorphisms componentwise gives ${\mathrm{Tm}}_A\times {\mathrm{Tm}}_{A^{\prime }}\cong \mathrm{y}({\mathrm{\Delta }}_2)$, the component at $\mathrm{\Gamma }$ sending $(e,e^{\prime })$ to the substitution $(e,e^{\prime })$. Then corollary 141.53 with $r={\mathrm{\Delta }}_2$, $K={\mathrm{Tm}}_B$ gives $\mathrm{Nat}({\mathrm{Tm}}_A\times {\mathrm{Tm}}_{A^{\prime }},{\mathrm{Tm}}_B)\cong {\mathrm{Tm}}_B({\mathrm{\Delta }}_2)$, the terms $x:A,x^{\prime }:A^{\prime }⊢b:B$. The transformation of $b$ has components $(e,e^{\prime })\mapsto {\mathrm{Tm}}_B((e,e^{\prime }))(b)=b[e/x,e^{\prime }/x^{\prime }]$, and the term of a transformation $\alpha$ is ${\alpha }_{{\mathrm{\Delta }}_2}(x,x^{\prime })$. For $A=A^{\prime }\to B$, application $(e_1,e_2)\mapsto e_1{e}_2$ corresponds to ${\mathrm{app}}_{{\mathrm{\Delta }}_2}(x,x^{\prime })=x{x}^{\prime }$, and indeed $(x{x}^{\prime })[e_1/x,e_2/x^{\prime }]=e_1{e}_2$.

Regard $P$ as a category by example 141.15. A presheaf $K$ assigns a set $K(a)$ to each $a$ and a function $K(a\le b):K(b)\to K(a)$ to each $a\le b$, with $K(a\le a)={\mathrm{id}}_{K(a)}$ and $K(a\le c)=K(a\le b)\circ K(b\le c)$ for $a\le b\le c$. The representable $\mathrm{y}(r)$ has $\mathrm{y}(r)(a)={\mathrm{hom}}_P(a,r)$, a one-element set when $a\le r$ and empty otherwise: the down-set of $r$. A natural transformation $\varphi :\mathrm{y}(r)\Rightarrow K$ is a family of elements ${\varphi }_a\in K(a)$ for $a\le r$ (the value of ${\varphi }_a$ at the unique arrow), natural when $K(a\le b)({\varphi }_b)={\varphi }_a$ for all $a\le b\le r$: a compatible family over the down-set. Corollary 141.53 says such a family is determined by ${\varphi }_r\in K(r)$ through ${\varphi }_a=K(a\le r)({\varphi }_r)$, and every element of $K(r)$ arises. In chapter 49, the values at a context restrict along every extension, and the uniform action demanded there is exactly compatibility of the family; the lemma identifies a single value at $\mathrm{\Gamma }$ with its whole compatible family of restrictions.

If $a\sim a^{\prime }$ and $b\sim b^{\prime }$ then $a\le b$ implies $a^{\prime }\le a\le b\le b^{\prime }$, and symmetrically, so $[a]\le [b]$ does not depend on the representatives. It is reflexive and transitive because $\le$ is, and antisymmetric: $[a]\le [b]$ and $[b]\le [a]$ give $a\le b$ and $b\le a$, so $a\sim b$ and $[a]=[b]$. The quotient map $q(a):=[a]$ is monotone, hence a functor (example 141.33); it is faithful because hom-sets have at most one element, full because $[a]\le [b]$ means $a\le b$ by definition, and essentially surjective because every class is $q(a)$ for any of its members. By theorem 141.46 it is an equivalence. If $\le$ is antisymmetric then every class is a singleton, $q$ is a bijection on objects, and the map sending $[a]$ to its member is an inverse functor, monotone because $[a]\le [b]$ means $a\le b$; so $q$ is an isomorphism of categories. Conversely an isomorphism of categories is injective on objects, so $a\sim b$ implies $[a]=[b]$ implies $a=b$: antisymmetry. For the generality order, ${\sigma }_1\sim {\sigma }_2$ means ${\sigma }_1⊒{\sigma }_2$ and ${\sigma }_2⊒{\sigma }_1$, that is, every instance of each is an instance of the other: the two schemes have the same monotype instances, as $\mathrm{\forall }\alpha .\alpha \to \alpha$, $\mathrm{\forall }\beta .\beta \to \beta$, and $\mathrm{\forall }\alpha \mathrm{\forall }\beta .\alpha \to \alpha$ do.

$\tau \circ \sigma =((yv)[\sigma ])=((\lambda w:\mathbf{2}.uw)(u\mathsf{tt})):\mathrm{\Gamma }⟶\mathrm{\Theta }$. The range of $\tau \circ \sigma$ has free variable $u$, which is the bound name of $e:=\lambda u:\mathbf{2}.z$; so the abstraction clause renames it: $$(\lambda u:\mathbf{2}.z)[\tau \circ \sigma ]=\lambda u^{\prime }:\mathbf{2}.(\lambda w:\mathbf{2}.uw)(u\mathsf{tt}).$$ Separately, $e[\tau ]=\lambda u:\mathbf{2}.yv$ with no renaming, since $u$ is not free in $yv$; then applying $\sigma$, whose range again has $u$ free, renames the binder and gives $\lambda u^{\prime }:\mathbf{2}.(\lambda w:\mathbf{2}.uw)(u\mathsf{tt})$. The two results are identical, confirming lemma 141.5. A bound name changed at exactly the steps where a substitution whose range contains $u$ passed under the binder $u$: once in the composite action and once in the second of the two separate actions. Without the change, the free $u$ of $\mathrm{\Gamma }$ would have been captured and the result would have been closed.

For $R:A⟶B$ and $S:B⟶C$, and $({\mathrm{id}}_A{)}^{⌣}=\{(x,x)\}={\mathrm{id}}_A$. Define $F:\mathbf{Rel}\to {\mathbf{Rel}}^{\mathrm{op}}$ as the identity on objects and $F(R):=R^{⌣}$, an arrow $B⟶A$ of $\mathbf{Rel}$, hence an arrow $A⟶B$ of ${\mathbf{Rel}}^{\mathrm{op}}$. Functoriality: $F(S\circ R)=R^{⌣}\circ S^{⌣}$, and in ${\mathbf{Rel}}^{\mathrm{op}}$ the composite $F(S){\circ }^{\mathrm{op}}F(R)$ is $F(R)\circ F(S)=R^{⌣}\circ S^{⌣}$ by definition 141.25; identities are preserved by the second equation. Since $(R^{⌣}{)}^{⌣}=R$, $F$ is its own inverse, so it is an isomorphism of categories.

Define $\mathrm{\Theta }(g):={\mathrm{hom}}_{\mathcal{C}}(g,-)$ for $g:s⟶r$, with components ${\mathrm{hom}}_{\mathcal{C}}(r,a)\to {\mathrm{hom}}_{\mathcal{C}}(s,a)$, $h\mapsto h\circ g$; this is natural by associativity, as in the proof of theorem 141.52. Define the inverse $\mathrm{\Xi }(\varphi ):={\varphi }_r({\mathrm{id}}_r)\in {\mathrm{hom}}_{\mathcal{C}}(s,r)$ for natural $\varphi :{\mathrm{hom}}_{\mathcal{C}}(r,-)\Rightarrow {\mathrm{hom}}_{\mathcal{C}}(s,-)$. Then $\mathrm{\Xi }(\mathrm{\Theta }(g))={\mathrm{id}}_r\circ g=g$. For the other composite, let $\varphi$ be natural, $a$ an object, $h:r⟶a$; naturality of $\varphi$ at $h$, evaluated at ${\mathrm{id}}_r$, gives ${\varphi }_a(h\circ {\mathrm{id}}_r)=h\circ {\varphi }_r({\mathrm{id}}_r)$, i.e. ${\varphi }_a(h)=h\circ \mathrm{\Xi }(\varphi )=\mathrm{\Theta }(\mathrm{\Xi }(\varphi ){)}_a(h)$. So $\mathrm{\Theta }$ and $\mathrm{\Xi }$ are mutually inverse. The assignment $r\mapsto {\mathrm{hom}}_{\mathcal{C}}(r,-)$, $g\mapsto {\mathrm{hom}}_{\mathcal{C}}(g,-)$ is a functor ${\mathcal{C}}^{\mathrm{op}}\to [\mathcal{C},\mathbf{Set}]$: an arrow $r⟶s$ of ${\mathcal{C}}^{\mathrm{op}}$ is $g:s⟶r$, and ${\mathrm{hom}}_{\mathcal{C}}(g^{\prime }\circ g,-)={\mathrm{hom}}_{\mathcal{C}}(g,-)\circ {\mathrm{hom}}_{\mathcal{C}}(g^{\prime },-)$ componentwise, $h\mapsto h\circ g^{\prime }\circ g$, which is the composite in the order required by ${\mathcal{C}}^{\mathrm{op}}$. The bijection just proved says this functor is injective and surjective on each hom-set, that is, fully faithful.

Let $\alpha :F\Rightarrow G$, $\beta :G\Rightarrow H$, $\gamma :H\Rightarrow J$. Associativity asserts $(\gamma \circ \beta )\circ \alpha =\gamma \circ (\beta \circ \alpha )$ as natural transformations $F\Rightarrow J$; two natural transformations are equal when all their components are, and at $a$ the two sides are $({\gamma }_a\circ {\beta }_a)\circ {\alpha }_a$ and ${\gamma }_a\circ ({\beta }_a\circ {\alpha }_a)$, equal by associativity in $\mathcal{D}$. The unit laws ${\mathrm{id}}_G\circ \alpha =\alpha =\alpha \circ {\mathrm{id}}_F$ reduce at $a$ to ${\mathrm{id}}_{G(a)}\circ {\alpha }_a={\alpha }_a={\alpha }_a\circ {\mathrm{id}}_{F(a)}$, the unit laws of $\mathcal{D}$. That the composites are natural was shown in section 141.7, so the laws are equations between arrows of $[\mathcal{C},\mathcal{D}]$.

$w$ is a substitution because $\mathrm{\Gamma },x:A⊢x_i:A_i$ by Var. Its action on a $\mathrm{\Gamma }$-term $e$ is $e[x_1/x_1,\dots ,x_n/x_n]=e$ by lemma 141.2(2), the same term regarded in the larger context; so the action is injective.

Epic. Let $v,v^{\prime }:\mathrm{\Gamma }⟶\mathrm{\Theta }$ with $v\circ w=v^{\prime }\circ w$. Componentwise, $v(z_k)[w]=v^{\prime }(z_k)[w]$, and by the remark just made this is $v(z_k){=}_{\alpha }{v}^{\prime }(z_k)$; so $v=v^{\prime }$.

Not monic. Let $\mathrm{\Lambda }:=\mathrm{\Gamma },x:A,x^{\prime }:A$ and $u:=(x_1,\dots ,x_n,x)$, $u^{\prime }:=(x_1,\dots ,x_n,x^{\prime })$, both substitutions $\mathrm{\Lambda }⟶\mathrm{\Gamma },x:A$. Then $w\circ u=(x_1,\dots ,x_n)=w\circ u^{\prime }$, since $w$ has no component for $x$, but $u\ne u^{\prime }$.

Not an isomorphism. An isomorphism $f$ with inverse $g$ is monic: $f\circ u=f\circ u^{\prime }$ gives $u=g\circ f\circ u=g\circ f\circ u^{\prime }=u^{\prime }$. Since $w$ is not monic, it is not an isomorphism.

The epimorphism argument used only the injectivity of the action: if $e[w]=e^{\prime }[w]$ then $e=e^{\prime }$. The global-element argument of proposition 141.29 separated two arrows into $A$ by evaluating them at elements $1\to A$. In $\mathbf{Ctx}$ take $A=P$ atomic: the source $\mathrm{\Gamma },x:P$ of $w$ has no global elements, because a global element would include a closed term of type $P$, and by theorem 2.43 and lemma 2.59 a closed normal term has a non-atomic type or a free variable. So the test “$w\circ \rho =w\circ {\rho }^{\prime }$ implies $\rho ={\rho }^{\prime }$” at $t=\cdot$ holds vacuously while $w$ is not monic; cancellation in $\mathbf{Ctx}$ must be tested against arbitrary contexts, as the definition requires.

An arrow $(a,b)⟶(a^{\prime },b^{\prime })$ of $P\times Q$ is a pair of an arrow $a\le a^{\prime }$ and an arrow $b\le b^{\prime }$, which exists exactly when both relations hold and is then unique; so $P\times Q$ has at most one arrow between any two objects and is the preorder described, by example 141.15. On a preorder, ${\mathrm{hom}}_P(a,b)$ is a one-element set when $a\le b$ and empty otherwise, and ${\mathrm{hom}}_P(f,g)$ for $f:a^{\prime }\le a$, $g:b\le b^{\prime }$ is the unique function between the corresponding sets, which exists because $a\le b$ implies $a^{\prime }\le a\le b\le b^{\prime }$. Functoriality is automatic. For a functor $K:P^{\mathrm{op}}\times P\to \mathbf{Set}$ with empty or one-element values, define the canonical functor $\hat{K}$ by $\hat{K}(a,b)=1$ when $K(a,b)$ is inhabited and $\hat{K}(a,b)=\mathrm{\varnothing }$ otherwise. The function on objects $(a,b)\mapsto [K(a,b)\ne \mathrm{\varnothing }]$ is monotone into $\{0\le 1\}$: a function $K(a,b)\to K(a^{\prime },b^{\prime })$ can exist only when $K(a,b)=\mathrm{\varnothing }$ or $K(a^{\prime },b^{\prime })\ne \mathrm{\varnothing }$. Conversely a monotone truth-value map defines such a canonical functor, with every arrow action the unique function between the corresponding empty or singleton sets. The unique bijection $K(a,b)\to \hat{K}(a,b)$ at each object is natural, since every square is between sets with at most one element. Thus $K$ and $\hat{K}$ are naturally isomorphic; they need not be literally equal when $K$ uses noncanonical singleton sets. Under this correspondence the hom bifunctor is naturally isomorphic to the functor classified by the map sending $(a,b)$ to $1$ iff $a\le b$: it is monotone because $(a,b)\le (a^{\prime },b^{\prime })$ in $P^{\mathrm{op}}\times P$ means $a^{\prime }\le a$ and $b\le b^{\prime }$, and then $a\le b$ implies $a^{\prime }\le b^{\prime }$.

${\mathrm{hom}}_{\mathcal{C}}(1,-)$ sends $f:a⟶b$ to the function $u\mapsto f\circ u$ on global elements. It is faithful exactly when $f\ne f^{\prime }$ implies that these functions differ, that is, that some $u$ has $f\circ u\ne f^{\prime }\circ u$: this is the definition of having enough points. $\mathbf{Set}$ has enough points because $f\ne f^{\prime }$ means $f(x)\ne f^{\prime }(x)$ for some $x$, and then $f\circ \underset{―}{x}\ne f^{\prime }\circ \underset{―}{x}$. In $\mathbf{Ctx}$, let $P$ be atomic. The substitutions $(\mathsf{tt}),(\mathsf{ff}):⟨P⟩⟶⟨\mathbf{2}⟩$ are distinct. A global element of $⟨P⟩$ is a closed term of type $P$, and there is none: such a term would reduce, by theorem 2.43 and subject reduction (corollary 2.44), to a closed normal term of type $P$, which by lemma 2.59 is an introduction form, whose type is never atomic, or variable-headed, which needs a free variable. So the two substitutions agree on every environment vacuously, and $\mathbf{Ctx}$ does not have enough points.

Let $\eta :\mathrm{Id}\Rightarrow G\circ F$, $\epsilon :F\circ G\Rightarrow \mathrm{Id}$, ${\eta }^{\prime }:\mathrm{Id}\Rightarrow G^{\prime }\circ F$, ${\epsilon }^{\prime }:F\circ G^{\prime }\Rightarrow \mathrm{Id}$ be the given natural isomorphisms. Define ${\theta }_d:=G^{\prime }({\epsilon }_d)\circ {\eta }_{G(d)}^{\prime }:G(d)⟶G^{\prime }(F(G(d)))⟶G^{\prime }(d)$. Each component is an isomorphism: ${\eta }_{G(d)}^{\prime }$ is one, and $G^{\prime }({\epsilon }_d)$ is one with inverse $G^{\prime }({\epsilon }_d^{-1})$, by (141.4). Naturality at $g:d⟶d^{\prime }$: So $\theta$ is a natural isomorphism $G\Rightarrow G^{\prime }$ by proposition 141.43.

Let $(r,u)$ and $(r^{\prime },u^{\prime })$ be two representations, so both are terminal objects of $\int K$ by proposition 141.65. By lemma 141.27 they are isomorphic in $\int K$ by a unique isomorphism $f:(r,u)⟶(r^{\prime },u^{\prime })$ with inverse $f^{\prime }$. The arrows of $\int K$ are arrows of $\mathcal{C}$ composed as in $\mathcal{C}$, so $f:r⟶r^{\prime }$ and $f^{\prime }:r^{\prime }⟶r$ satisfy $f^{\prime }\circ f={\mathrm{id}}_r$ and $f\circ f^{\prime }={\mathrm{id}}_{r^{\prime }}$ in $\mathcal{C}$, because the projection ${\pi }_K$ is the identity on arrows and composition in $\int K$ is that of $\mathcal{C}$. Hence $r\cong r^{\prime }$, which is the uniqueness stated in corollary 141.59; moreover $f$ satisfies $K(f)(u^{\prime })=u$, so it carries one universal element to the other.

An object of $\int \mathrm{Env}$ is a pair $(\mathrm{\Gamma },\rho )$ of a context and an environment $\rho :\cdot ⟶\mathrm{\Gamma }$ for it. An arrow $(\mathrm{\Gamma },\rho )⟶(\mathrm{\Delta },{\rho }^{\prime })$ is a substitution $\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }$ with $\mathrm{Env}(\sigma )(\rho )=\sigma \circ \rho ={\rho }^{\prime }$: a substitution that carries the first environment to the second. The object $(\cdot ,())$, the empty context with the empty environment, is initial: an arrow $(\cdot ,())⟶(\mathrm{\Gamma },\rho )$ is a substitution $\sigma :\cdot ⟶\mathrm{\Gamma }$ with $\sigma \circ ()=\rho$, and $\sigma \circ ()=\sigma$ since $()$ is ${\mathrm{id}}_{\cdot }$, so $\sigma =\rho$ is the unique such arrow. This is the dual of the terminal object $(⟨A⟩,x)$ of $\int {\mathrm{Tm}}_A$: the covariant functor $\mathrm{Env}={\mathrm{hom}}_{\mathbf{Ctx}}(\cdot ,-)$ is represented by $\cdot$, and its category of elements has an initial object, the universal element $()$.

Suppose $\varphi :\mathrm{y}(\mathrm{\Delta })\Rightarrow K$ is a natural isomorphism. By proposition 141.43 its component at $\cdot$ is a bijection ${\mathrm{hom}}_{\mathbf{Ctx}}(\cdot ,\mathrm{\Delta })\to K(\cdot )=\{0,1\}$, so ${\mathrm{hom}}_{\mathbf{Ctx}}(\cdot ,\mathrm{\Delta })$ has exactly two elements. These elements are lists of closed terms $(\cdot ⊢a_j:B_j{)}_j$.

If $\mathrm{\Delta }=\cdot$, the only list is the empty one: one element. Otherwise, if some declared type $B_j$ has no closed term, the hom-set is empty. This happens for an atomic type $P$: a closed term of type $P$ would, by strong normalization (theorem 2.43) and subject reduction (corollary 2.44), reduce to a closed normal term $n$ of type $P$, and by lemma 2.59 $n$ is either an introduction form, whose type is never atomic, or is variable-headed, which requires a free variable; neither has type $P$ in the empty context, the argument of corollary 2.44. If every $B_j$ has a closed term $t_j$, then the hom-set is infinite: the terms $t_1,(\lambda y:B_1.y)t_1,(\lambda y:B_1.y)((\lambda y:B_1.y)t_1),\dots$ are closed, of type $B_1$ by Lam and App, and pairwise distinct as syntax trees, hence as $\alpha$-classes, since their sizes differ; each gives a different list. In every case the count is not two, so no representation exists. Note that ${\mathrm{Tm}}_A$ counts terms up to $\alpha$-equivalence only; the argument would change for terms up to $\beta \eta$-equality.