Categories, Functors, and Representability

Three facts have been proved separately in this book, each about a different kind of composition. Type substitutions compose in diagrammatic order and $\mathrm{id}$ is a two-sided unit for that composition (definition 3.5). Simultaneous term substitutions act on terms, and extending a substitution by one more variable is the same as acting twice (equation 2.1). Context extensions $\mathrm{\Delta }⊵\mathrm{\Gamma }$ compose, and a semantic value at $\mathrm{\Gamma }$ must act uniformly at every extension (chapter 49). Each proof is a short induction, and each is repeated whenever a new calculus arrives. The repetition is not harmless: comparing a syntax with its environments, or a calculus with a model, requires saying that two such composition structures agree, and that statement cannot be made until both structures are instances of one definition. The object that removes the repetition is a set of arrows with a typed composition satisfying three equations.

Substitutions compose

Fix the simply typed calculus of chapter 2: types $A,B::=P\mid \mathbf{2}\mid A\to B$; terms built from variables, abstraction, application, the constants $\mathsf{tt},\mathsf{ff}$, and the conditional $\mathsf{if}(e;e_1;e_2)$, typed by the rules Var, Lam, App, and the Boolean rules; and simultaneous capture-avoiding substitution $e[\sigma ]$ from definition 2.41. A context $\mathrm{\Gamma }=x_1:A_1,\dots ,x_n:A_n$ declares distinct variables. As in convention 2.3, a term is an $\alpha$-equivalence class, so equality of terms is equality up to renaming of bound variables; the symbol ${=}_{\alpha }$ marks the places where a calculation is performed on representatives.

A substitution $\mathrm{\Gamma }⟶\mathrm{\Delta }$ provides a $\mathrm{\Gamma }$-term for each variable of $\mathrm{\Delta }$, so its action sends $\mathrm{\Delta }$-terms to $\mathrm{\Gamma }$-terms: the arrow and the action point in opposite directions. Chapter 26 wrote $f:\mathrm{\Gamma }\Rightarrow \mathrm{\Delta }$ for the dependent form of the same list (definition 26.45); here it is written with the arrow $⟶$.

Three facts about substitution are used repeatedly and are stated once.

Proof of Lemma 141.2 — Trivial substitutions

Proof. All three are proved by induction on $e$, choosing each bound name fresh for $y$, for the $x_i$, and for the range of $\theta$. At a variable, both sides of (1) are $y$ if the variable is $y$ and the value of $\theta$ otherwise; both sides of (2) are the variable itself; and in (3) the variable is free in $e$, hence outside the domain, and is unchanged. Application, the constants, and the conditional recurse in their immediate subterms, the hypothesis of (3) passing to each subterm because its free variables are among those of $e$. At an abstraction $\lambda z:B.b$ with $z$ fresh, the abstraction clause of definition 2.41 removes $z$ from the domain on both sides; for (3) the free variables of $b$ are those of $e$ together with $z$, which is not in the domain of $\theta \setminus z$, so the induction hypothesis applies to $b$, and $\lambda z$ is reattached. ◻

Proof of Lemma 141.3 — Action preserves typing

Proof. Induct on the derivation of $\mathrm{\Delta }⊢e:A$, proving the statement for every $\mathrm{\Gamma }$ and every $\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }$ at once.

Variable case. The term is $y_j$ with $A=B_j$, and $y_j[\sigma ]=b_j$, which has type $B_j$ in $\mathrm{\Gamma }$ by the definition of a substitution.

Application case. From $\mathrm{\Delta }⊢e_1:B\to A$ and $\mathrm{\Delta }⊢e_2:B$ the induction hypothesis gives $\mathrm{\Gamma }⊢e_1[\sigma ]:B\to A$ and $\mathrm{\Gamma }⊢e_2[\sigma ]:B$, and App derives the type of $e_1[\sigma ]e_2[\sigma ]=(e_1{e}_2)[\sigma ]$. The constants are unchanged by substitution and keep their type; the conditional recurses in its three subterms exactly as application does.

Binder case. The term is $\lambda y:B.b$ with $\mathrm{\Delta },y:B⊢b:C$ and $A=B\to C$. Choose the bound name $y$ fresh for $\mathrm{\Gamma }$, for $\mathrm{\Delta }$, and for every $b_j$; convention 2.3 permits this. The list ${\sigma }^{+}:=(b_1,\dots ,b_m,y)$ is then a substitution $\mathrm{\Gamma },y:B⟶\mathrm{\Delta },y:B$: each $b_j$ keeps its type by lemma 2.14, and $y$ has type $B$ by Var. The induction hypothesis for $b$ at ${\sigma }^{+}$ gives $\mathrm{\Gamma },y:B⊢b[{\sigma }^{+}]:C$, and $b[{\sigma }^{+}]=b[\sigma ]$ by lemma 141.2(1). Then Lam derives $\mathrm{\Gamma }⊢\lambda y:B.b[\sigma ]:B\to C$, whose subject is $(\lambda y:B.b)[\sigma ]$ by the abstraction clause of definition 2.41. ◻

Both lists are substitutions: $\mathrm{\Gamma }⊢c_k[\sigma ]:C_k$ by lemma 141.3, and $\mathrm{\Gamma }⊢x_i:A_i$ by Var. Compute one composite before proving anything about it. Let $$\mathrm{\Gamma }=f:\mathbf{2}\to \mathbf{2},x:\mathbf{2},\mathrm{\Delta }=y:\mathbf{2},\mathrm{\Theta }=z:\mathbf{2}\to \mathbf{2},$$ and take $\sigma =(fx):\mathrm{\Gamma }⟶\mathrm{\Delta }$ and $\tau =(\lambda w:\mathbf{2}.y):\mathrm{\Delta }⟶\mathrm{\Theta }$. Then $$\tau \circ \sigma =((\lambda w:\mathbf{2}.y)[(fx)/y])=(\lambda w:\mathbf{2}.fx):\mathrm{\Gamma }⟶\mathrm{\Theta }.$$ Now let $\mathrm{\Theta }⊢e:\mathbf{2}$ be $e:=z\mathsf{tt}$ and compare the two ways of reaching a $\mathrm{\Gamma }$-term: They agree. The composite $\tau \circ \sigma$ is “first $\sigma$, then $\tau$” as arrows, and its action on terms is “first $\tau$, then $\sigma$”. That the two calculations always agree is the following lemma.

Proof of Lemma 141.5 — Action law

Proof. Induct on $e$, proving the equation for all $\mathrm{\Gamma },\mathrm{\Delta },\mathrm{\Theta }$ and all $\sigma ,\tau$ at once, and choosing every bound name fresh for $\mathrm{\Gamma }$, $\mathrm{\Delta }$, $\mathrm{\Theta }$, and the ranges of $\sigma$, $\tau$, and $\tau \circ \sigma$ (convention 2.3).

Variable case. For $e=z_k$, $$z_k[\tau \circ \sigma ]\stackrel{def.\circ }{=}{c}_k[\sigma ]\stackrel{def.action}{=}{z}_k[\tau ][\sigma ].$$

Application case. For $e=e_1{e}_2$ and any substitution $\theta$, $(e_1{e}_2)[\theta ]=e_1[\theta ]e_2[\theta ]$ by the application clause, so both sides are applications whose two components are equal by the induction hypotheses for $e_1$ and $e_2$. The constants are fixed by every substitution, and the conditional recurses in its three subterms as application does.

Binder case. For $e=\lambda y:B.b$ with $y$ fresh as above, $y$ lies in the domain of neither substitution, so the abstraction clause of definition 2.41 reads $(\lambda y:B.b)[\theta ]=\lambda y:B.b[\theta ]$ for $\theta \in \{\tau \circ \sigma ,\tau ,\sigma \}$. Write ${\sigma }^{+}:=(\sigma ,y\mapsto y)$ and ${\tau }^{+}:=(\tau ,y\mapsto y)$, substitutions $\mathrm{\Gamma },y:B⟶\mathrm{\Delta },y:B$ and $\mathrm{\Delta },y:B⟶\mathrm{\Theta },y:B$. Two facts are used:

1. $t[\theta ]=t[{\theta }^{+}]$ for every term $t$ and each $\theta$, by lemma 141.2(1), since $y$ is in no domain;

2. $(\tau \circ \sigma {)}^{+}={\tau }^{+}\circ {\sigma }^{+}$ componentwise: at $z_k$ the left side is $c_k[\sigma ]$ and the right side is $c_k[{\sigma }^{+}]$, equal by (1); at $y$ both sides are $y$.

Then the induction hypothesis being applied to $b$ with the substitutions ${\sigma }^{+}$ and ${\tau }^{+}$. ◻

Proof of Proposition 141.7 — The substitution algebra

Proof. Let $\mathrm{\Lambda }=w_1:D_1,\dots ,w_p:D_p$ and $\rho =(d_1,\dots ,d_p)$. Compare the $k$-th components: $$((\rho \circ \tau )\circ \sigma )(w_k)\stackrel{def.}{=}{d}_k[\tau ][\sigma ]\stackrel{actionlaw}{=}{d}_k[\tau \circ \sigma ]\stackrel{def.}{=}(\rho \circ (\tau \circ \sigma ))(w_k).$$ For the identities, $({\mathrm{id}}_{\mathrm{\Delta }}\circ \sigma )(y_j)=y_j[\sigma ]=b_j$ by the variable clause, and $(\sigma \circ {\mathrm{id}}_{\mathrm{\Gamma }})(y_j)=b_j[x_1/x_1,\dots ,x_n/x_n]=b_j$ by lemma 141.2(2). ◻

Proposition 141.7 mentions neither terms nor the action: it is three equations between composites of arrows. The definition that follows records what the proposition uses: objects, typed arrows, composition, identities, and the three equations; nothing else. The action $e[\sigma ]$ is not part of it; it returns in section 141.6 as additional structure over a category.

The definition

Composition is written in the order of functions, $g\circ f$ meaning “first $f$, then $g$”; chapter 3 wrote the composition of type substitutions in the opposite, diagrammatic order $S;T$. Each hom-set is a set; the objects need not form a set, and a category whose objects do form a set is called small. Size is noted at the places where it matters.

A category is a monoid whose multiplication is typed. In $\mathbf{Ctx}$ the product $\tau \circ \sigma$ exists only when the target of $\sigma$ is the source of $\tau$: in (141.1) the middle context $\mathrm{\Delta }$ is what makes the two lists fit, and $(fx):\mathrm{\Gamma }⟶\mathrm{\Delta }$ has no composite with an arrow out of any other context. The objects are the types of this partial multiplication. With one object the typing is vacuous.

Proof of Proposition 141.11 — One-object categories

Proof. With one object, every pair of arrows is composable, so $\circ$ is a total binary operation on $M$, and (141.2) says precisely that it is associative with two-sided unit ${\mathrm{id}}_{\ast }$. Conversely, the monoid axioms for $(M,\cdot ,e)$ are (141.2) with $a=b=c=d=\ast$. ◻

Besides the three equations, the definition asks for two things: an identity arrow at every object, and a composite for every two arrows whose types match. For a subcollection of the arrows of $\mathbf{Ctx}$ these are closure conditions. The following three examples keep the objects of $\mathbf{Ctx}$ and restrict the arrows: the first restriction is a category, the second has no identities, and the third is not closed under composition.

Three further examples change what an arrow carries rather than which arrows there are.

The construction of $\mathbf{Paths}$ used nothing about reduction except that it is a relation on terms: a set of vertices and a set of edges.

$\mathbf{Paths}$ is the free category on the graph whose vertices are terms and whose edges are the one-step reductions.

Isomorphisms, duality, and terminal objects

Proof of Lemma 141.22 — Inverses are unique

Proof. $$g\stackrel{unit}{=}g\circ {\mathrm{id}}_b\stackrel{hyp.}{=}g\circ (f\circ g^{\prime })\stackrel{assoc.}{=}(g\circ f)\circ g^{\prime }\stackrel{hyp.}{=}{\mathrm{id}}_a\circ g^{\prime }\stackrel{unit}{=}{g}^{\prime }.$$ ◻

The inverse of an isomorphism $f$ is therefore well defined and is written $f^{-1}$. In $\mathbf{Set}$ the isomorphisms are the bijections; in a preorder $a\cong b$ means $a\le b$ and $b\le a$; in a one-object category they are the invertible elements of the monoid.

The paths $p:a=b$ of chapter 30 compose, have inverses $p^{-1}$, and satisfy the laws of a category up to higher paths. The strict form of that structure has a name.

A one-object groupoid is a group: by proposition 141.11 it is a monoid, and every element has an inverse. A preorder is a groupoid exactly when its relation is symmetric, that is, an equivalence relation: the arrow $a\le b$ has an inverse only if $b\le a$, and conversely when $b\le a$ the two composites are identities because each hom-set has at most one element. Every category $\mathcal{C}$ contains a groupoid with the same objects, whose arrows are the isomorphisms of $\mathcal{C}$: identities are isomorphisms, and the composite of isomorphisms $f,g$ is an isomorphism with inverse $f^{-1}\circ g^{-1}$. For $\mathbf{Ctx}$, exercise 141.3 identifies these arrows as the permutation-renamings.

Every definition of this section has a mirror image obtained by reversing all arrows, and the reversal is itself a category.

The laws for ${\mathcal{C}}^{\mathrm{op}}$ follow from those of $\mathcal{C}$; for associativity, $$(h{\circ }^{\mathrm{op}}g){\circ }^{\mathrm{op}}f\stackrel{def.}{=}f\circ (g\circ h)\stackrel{assoc.}{=}(f\circ g)\circ h\stackrel{def.}{=}h{\circ }^{\mathrm{op}}(g{\circ }^{\mathrm{op}}f),$$ and the unit laws likewise; also $({\mathcal{C}}^{\mathrm{op}}{)}^{\mathrm{op}}=\mathcal{C}$. An arrow $a⟶b$ in ${\mathcal{C}}^{\mathrm{op}}$ is an arrow $b⟶a$ in $\mathcal{C}$; nothing else changes. A statement $S$ about an arbitrary category, formulated in terms of objects, arrows, composition, and identities, has a dual statement $S^{\mathrm{op}}$ obtained by reversing every arrow and every composite. If $S$ holds in every category, then so does $S^{\mathrm{op}}$: applying $S$ to ${\mathcal{C}}^{\mathrm{op}}$ yields $S^{\mathrm{op}}$ for $\mathcal{C}$. Lemma 141.27 is proved once and used twice in this way. Concretely, for $R\subseteq A\times B$ put $R^{⌣}:=\{(b,a)\mid (a,b)\in R\}$. Directly from example 141.19, $$(S\circ R{)}^{⌣}=R^{⌣}\circ S^{⌣},{\mathrm{id}}_A^{⌣}={\mathrm{id}}_A,(R^{⌣}{)}^{⌣}=R.$$ Thus converse is an isomorphism $\mathbf{Rel}\to {\mathbf{Rel}}^{\mathrm{op}}$ that is the identity on objects and is its own inverse. A preorder’s opposite is the same set with $\le$ reversed.

Proof of Lemma 141.27 — Uniqueness up to isomorphism

Proof. Let $1$ and $1^{\prime }$ be terminal and let $t:1⟶1^{\prime }$ and $t^{\prime }:1^{\prime }⟶1$ be the unique arrows. Then $t^{\prime }\circ t:1⟶1$ and ${\mathrm{id}}_1$ are both arrows $1⟶1$, so they are equal by uniqueness; likewise $t\circ t^{\prime }={\mathrm{id}}_{1^{\prime }}$. Any isomorphism $1⟶1^{\prime }$ is an arrow $1⟶1^{\prime }$, hence equals $t$. The statement for initial objects is the dual. ◻

In $\mathbf{Ctx}$ the empty context $\cdot$ is terminal, the only substitution $\mathrm{\Gamma }⟶\cdot$ being the empty list. $\mathbf{Ctx}$ has no initial object: for any context $\mathrm{\Gamma }$, the two lists $(\mathsf{tt})$ and $(\mathsf{ff})$ are distinct substitutions $\mathrm{\Gamma }⟶⟨\mathbf{2}⟩$, where $⟨A⟩:=(x:A)$ denotes the one-declaration context; so no hom-set out of $\mathrm{\Gamma }$ into $⟨\mathbf{2}⟩$ has exactly one element. In $\mathbf{Set}$ a one-element set is terminal and the empty set is initial; in a preorder a greatest element is terminal and a least element is initial.

Cancellation and test objects

Injectivity of a function $f:A\to B$ is a statement about elements: $f(x)=f(x^{\prime })$ implies $x=x^{\prime }$. In a category there are no elements, only arrows, so the statement must be made about arrows into $A$.

The quantifier over $t$ is the point: $f$ is monic when it cannot identify two arrows from any test object $t$. An epimorphism in $\mathcal{C}$ is a monomorphism in ${\mathcal{C}}^{\mathrm{op}}$: the two notions are dual, and every fact proved about one for all categories holds for the other. In $\mathbf{Set}$ one test object suffices for each.

Proof of Proposition 141.29 — Cancellation in

Proof. Let $1:=\{\ast \}$ be a one-element set. A function $u:1\to A$ is determined by the single element $u(\ast )\in A$, and every element $x\in A$ is $u(\ast )$ for exactly one such $u$, namely the constant function at $x$, written $\underset{―}{x}$. Then $$f\circ \underset{―}{x}=\underset{―}{f(x)}.$$

Suppose $f$ is monic and $f(x)=f(x^{\prime })$. Then $$f\circ \underset{―}{x}\stackrel{(141.3)}{=}\underset{―}{f(x)}\stackrel{hyp.}{=}\underset{―}{f(x^{\prime })}\stackrel{(141.3)}{=}f\circ \underset{―}{x^{\prime }},$$ so $\underset{―}{x}=\underset{―}{x^{\prime }}$ by cancellation at $t=1$, and $x=x^{\prime }$. Conversely suppose $f$ injective and $f\circ u=f\circ u^{\prime }$ for $u,u^{\prime }:t\to A$. For each $s\in t$, $f(u(s))=f(u^{\prime }(s))$, so $u(s)=u^{\prime }(s)$; hence $u=u^{\prime }$.

Let $2:=\{0,1\}$. Suppose $f$ is epic and let $y\in B$; define $v,v^{\prime }:B\to 2$ by $v(z)=1$ for all $z$, and $v^{\prime }(z)=1$ if $z$ is in the image of $f$ and $v^{\prime }(z)=0$ otherwise. Then $v\circ f=v^{\prime }\circ f$, both being constantly $1$ on $A$, so $v=v^{\prime }$ by cancellation at $t=2$; evaluating at $y$ gives $v^{\prime }(y)=1$, so $y$ is in the image of $f$. Conversely suppose $f$ surjective and $v\circ f=v^{\prime }\circ f$ for $v,v^{\prime }:B\to t$. For each $y\in B$ choose $x$ with $f(x)=y$; then $v(y)\stackrel{choice}{=}v(f(x))\stackrel{hyp.}{=}{v}^{\prime }(f(x))\stackrel{choice}{=}{v}^{\prime }(y)$, so $v=v^{\prime }$. ◻

The proof used two facts about $\mathbf{Set}$: arrows $1\to A$ are the elements of $A$, and arrows $B\to 2$ are the subsets of $B$. Each is a statement that a set-theoretic notion is represented by maps from or to one fixed test object.

In $\mathbf{Set}$ the global elements of $A$ are its elements. In $\mathbf{Ctx}$ a global element $\cdot ⟶\mathrm{\Gamma }$ is a list of closed terms $(\cdot ⊢a_i:A_i{)}_i$, one for each declaration of $\mathrm{\Gamma }$. Call such a list an environment for $\mathrm{\Gamma }$: it assigns a closed term to each variable, as the environments $\eta$ of chapter 12 assign an element of a domain to each variable. Evaluating $\mathrm{\Gamma }⊢e:A$ in the environment $\rho$ is the action $e[\rho ]$, a closed term.

In $\mathbf{Set}$ an arrow that is both monic and epic is a bijection, hence an isomorphism. In a preorder this fails: every arrow $a\le b$ is monic and epic, the hom-sets having at most one element, and it is an isomorphism only when also $b\le a$. It also fails when arrows carry data.

Proof of Proposition 141.31 — Monic and epic but not invertible

Proof. $i$ is injective, hence monic by the argument of proposition 141.29, which used only that arrows are functions. It is not an isomorphism: an inverse $j:\mathbb{Z}⟶\mathbb{N}$ would be a homomorphism with $j\circ i={\mathrm{id}}_{\mathbb{N}}$, and $$j(1)+j(-1)\stackrel{hom.}{=}j(1+(-1))=j(0)\stackrel{hom.}{=}0$$ gives $j(1)=0$ in $\mathbb{N}$, since $0$ is the only element of $\mathbb{N}$ with an additive inverse, while $j(1)=j(i(1))=1$.

To see that $i$ is epic, let $v,v^{\prime }:\mathbb{Z}⟶M$ be homomorphisms with $v\circ i=v^{\prime }\circ i$, that is, $v(n)=v^{\prime }(n)$ for all $n\ge 0$. For $n\ge 0$, $$v(-n)\cdot v(n)\stackrel{hom.}{=}v(-n+n)=v(0)\stackrel{hom.}{=}e,v(n)\cdot v(-n)=e$$ likewise, so $v(-n)$ is a two-sided inverse of $v(n)$ in $M$. The same holds for $v^{\prime }(-n)$ and $v^{\prime }(n)=v(n)$. Inverses in a monoid are unique, by the calculation of lemma 141.22 read in the one-object category of $M$. Hence $v(-n)=v^{\prime }(-n)$, and $v=v^{\prime }$. ◻

Functors

A monoid homomorphism preserves the multiplication and the unit. The corresponding notion for categories preserves composition and identities, and must also respect the typing of arrows.

A functor out of a free category is determined by its values on the edges, and any choice of values extends to one.

Proof of Proposition 141.35 — Functors out of a free category

Proof. A path is a composite of its edges, ${ϵ}_n\circ \cdots \circ {ϵ}_1$, and the empty path is an identity, so a functor $F$ must send the path to $F({ϵ}_n)\circ \cdots \circ F({ϵ}_1)$ and the empty path to ${\mathrm{id}}_{F(v)}$; this fixes $F$ on every arrow. Conversely that assignment is a functor: it sends the empty path to an identity, and it sends the concatenation of two paths to the composite of their images. When one of the paths is empty this is a unit law in $\mathcal{D}$; when both are nonempty, both sides are the composite of the same sequence of edge images, bracketed in two ways, and repeated use of associativity in $\mathcal{D}$ identifies any two bracketings of one sequence. ◻

For example, the assignment sending every term to the single object $\ast$ and every one-step reduction to $1$ in the one-object category of the monoid $(\mathbb{N},+,0)$ extends to the functor $\mathbf{Paths}\to (\mathbb{N},+,0)$ that sends a reduction sequence to its length.

The functor that relates syntax to environments is the following. For a context $\mathrm{\Gamma }$, let $\mathrm{Env}(\mathrm{\Gamma }):={\mathrm{hom}}_{\mathbf{Ctx}}(\cdot ,\mathrm{\Gamma })$ be the set of environments for $\mathrm{\Gamma }$, its global elements. A substitution $\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }$ turns an environment for $\mathrm{\Gamma }$ into one for $\mathrm{\Delta }$: if $\rho$ assigns closed terms to the variables of $\mathrm{\Gamma }$, then $\sigma \circ \rho$ assigns to $y_j$ the closed term $\sigma (y_j)[\rho ]$.

Proof of Proposition 141.36 — Environments form a functor

Proof. For $\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }$, $\tau :\mathrm{\Delta }⟶\mathrm{\Theta }$, and $\rho \in \mathrm{Env}(\mathrm{\Gamma })$, using the laws of proposition 141.7. ◻

Nothing in that proof mentioned terms. Replacing $\cdot$ by any object $r$ of any category gives the same functor.

Proof of Proposition 141.37 — Hom-functors

Proof. The calculation of proposition 141.36 with $\cdot$ replaced by $r$: $(g\circ f)\circ u=g\circ (f\circ u)$ and ${\mathrm{id}}_a\circ u=u$. ◻

Functors compose: for $F:\mathcal{C}\to \mathcal{D}$ and $G:\mathcal{D}\to \mathcal{E}$, the assignments $a\mapsto G(F(a))$ and $f\mapsto G(F(f))$, written $G\circ F$, satisfy (141.4) because each of $F$ and $G$ does, and the identity assignment is a functor $\mathcal{C}\to \mathcal{C}$. Small categories and functors therefore form a category $\mathbf{Cat}$; the restriction to small categories keeps each hom-set a set.

Variance and presheaves

Environments vary with the context in the direction of the arrows. Terms vary against it. For a fixed type $A$ and a context $\mathrm{\Gamma }$, let $${\mathrm{Tm}}_A(\mathrm{\Gamma }):=\{e\mid \mathrm{\Gamma }⊢e:A\}$$ be the set of terms of type $A$ in context $\mathrm{\Gamma }$, up to $\alpha$-equivalence. A substitution $\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }$ acts by $e\mapsto e[\sigma ]$, which by lemma 141.3 is a function ${\mathrm{Tm}}_A(\mathrm{\Delta })\to {\mathrm{Tm}}_A(\mathrm{\Gamma })$, from the target of $\sigma$ to its source. The functor laws hold in this reversed form: lemma 141.5 says $e[\tau \circ \sigma ]=e[\tau ][\sigma ]$, and the identity law of proposition 141.7 says $e[{\mathrm{id}}_{\mathrm{\Gamma }}]=e$. Rather than a second definition of functor with the arrows reversed, the category is reversed: a functor out of ${\mathcal{C}}^{\mathrm{op}}$ (definition 141.25) is a functor that sends an arrow $a⟶b$ of $\mathcal{C}$ to an arrow from the image of $b$ to the image of $a$.

Proof of Proposition 141.39 — Terms form a presheaf

Proof. For $\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }$, $\tau :\mathrm{\Delta }⟶\mathrm{\Theta }$, and $e\in {\mathrm{Tm}}_A(\mathrm{\Theta })$, by lemma 141.5 and proposition 141.7. ◻

Presheaves combine pointwise. For presheaves $K,K^{\prime }$ on $\mathcal{C}$, the assignment $a\mapsto K(a)\times K^{\prime }(a)$ with $(K\times K^{\prime })(f)(u,u^{\prime }):=(K(f)(u),K^{\prime }(f)(u^{\prime }))$ satisfies (141.5) in each component, so it is a presheaf, the product $K\times K^{\prime }$. For types $A$ and $B$, the product ${\mathrm{Tm}}_{A\to B}\times {\mathrm{Tm}}_A$ has as value at $\mathrm{\Gamma }$ the set of pairs $(e_1,e_2)$ with $\mathrm{\Gamma }⊢e_1:A\to B$ and $\mathrm{\Gamma }⊢e_2:A$. Application sends such a pair to $e_1{e}_2\in {\mathrm{Tm}}_B(\mathrm{\Gamma })$ by App, and the application clause of definition 2.41 is the equation $$(e_1{e}_2)[\sigma ]=e_1[\sigma ]e_2[\sigma ]\text{for every }\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }.$$

A presheaf is a system of sets indexed by the objects and acted on contravariantly by the arrows. The semantic values of chapter 49, which are given at every context and restrict along every extension $\mathrm{\Delta }⊵\mathrm{\Gamma }$, are presheaves on the preorder of extensions of example 141.15, read with its arrow $\mathrm{\Delta }⟶\mathrm{\Gamma }$: restriction goes from the value at $\mathrm{\Gamma }$ to the value at $\mathrm{\Delta }$, against the arrow, and the restriction law $a{\upharpoonright }_{\mathrm{\Gamma }}=a$ together with the compatibility of successive restrictions is (141.5).

Natural transformations

Application is a family of functions ${\mathrm{app}}_{\mathrm{\Gamma }}:{\mathrm{Tm}}_{A\to B}(\mathrm{\Gamma })\times {\mathrm{Tm}}_A(\mathrm{\Gamma })\to {\mathrm{Tm}}_B(\mathrm{\Gamma })$, one for each context, and (141.6) says that substituting and then applying gives the same term as applying and then substituting: the family commutes with the action of every arrow. Other families of maps between term sets do not.

The condition that a family commute with every arrow is an equation between two composites, and such equations are often displayed as diagrams. The equation $g\circ f=k\circ h$ for $f:a⟶b$, $g:b⟶d$, $h:a⟶c$, $k:c⟶d$ is drawn as Diagram and the square is said to commute. A diagram is a directed graph whose vertices are objects and whose edges are arrows; it commutes when, for every two paths with the same start and end, the composites along the two paths are equal. A diagram is therefore a finite list of equations, one for each pair of parallel paths, and a diagram is always displayed together with the equations it abbreviates. The picture saves bookkeeping when several equations share arrows; it proves nothing by itself.

The arrow $\Rightarrow$ is the symbol chapter 26 used for context substitutions $f:\mathrm{\Gamma }\Rightarrow \mathrm{\Delta }$; here it relates two functors and never two contexts, which are related by $⟶$. Write $\mathrm{Nat}(F,G)$ for the collection of natural transformations $F\Rightarrow G$; when $\mathcal{C}$ is small, it is a set because its components form a $\mathcal{C}$-indexed family of sets.

Two instances outside syntax show the condition at its simplest. Between monotone maps $F,G:P\to Q$ of preorders, a natural transformation exists exactly when $F(a)\le G(a)$ for every $a$, and then it is unique: the components are the arrows $F(a)\le G(a)$, and (141.7) is automatic because ${\mathrm{hom}}_Q(F(a),G(b))$ has at most one element. In $\mathbf{Set}$, with $\mathrm{Id}$ the identity functor and $D(A):=A\times A$ on objects and $D(f)(x,y):=(f(x),f(y))$ on arrows, the diagonal ${\delta }_A(x):=(x,x)$ is natural $\mathrm{Id}\Rightarrow D$: $D(f)({\delta }_A(x))=(f(x),f(x))={\delta }_B(f(x))$.

For presheaves $K,K^{\prime }:{\mathcal{C}}^{\mathrm{op}}\to \mathbf{Set}$ the arrows reverse: $\alpha :K\Rightarrow K^{\prime }$ has components ${\alpha }_a:K(a)\to K^{\prime }(a)$ and naturality at $f:a⟶b$ in $\mathcal{C}$ reads $K^{\prime }(f)\circ {\alpha }_b={\alpha }_a\circ K(f)$ as functions $K(b)\to K^{\prime }(a)$.

Natural transformations compose componentwise. For $\alpha :F\Rightarrow G$ and $\beta :G\Rightarrow H$, set $(\beta \circ \alpha {)}_a:={\beta }_a\circ {\alpha }_a$. Naturality at $f:a⟶b$ is $$H(f)\circ {\beta }_a\circ {\alpha }_a\stackrel{nat.\beta }{=}{\beta }_b\circ G(f)\circ {\alpha }_a\stackrel{nat.\alpha }{=}{\beta }_b\circ {\alpha }_b\circ F(f),$$ and ${\mathrm{id}}_F$ with components ${\mathrm{id}}_{F(a)}$ is natural because both sides of (141.7) are $F(f)$. Associativity and the unit laws hold componentwise, so functors $\mathcal{C}\to \mathcal{D}$ and natural transformations form a category, the functor category $[\mathcal{C},\mathcal{D}]$, with ${\mathrm{hom}}_{[\mathcal{C},\mathcal{D}]}(F,G)=\mathrm{Nat}(F,G)$. Size matters here: $\mathrm{Nat}(F,G)$ is a family indexed by the objects of $\mathcal{C}$, and it is a set when $\mathcal{C}$ is small, which $\mathbf{Ctx}$ and every preorder in this chapter are. The presheaf category is $[{\mathcal{C}}^{\mathrm{op}},\mathbf{Set}]:=[{\mathcal{C}}^{\mathrm{op}},\mathbf{Set}]$.

Proof of Proposition 141.43 — Natural isomorphisms

Proof. If $\beta \circ \alpha ={\mathrm{id}}_F$ and $\alpha \circ \beta ={\mathrm{id}}_G$, then at each $a$ the components satisfy ${\beta }_a\circ {\alpha }_a={\mathrm{id}}_{F(a)}$ and ${\alpha }_a\circ {\beta }_a={\mathrm{id}}_{G(a)}$. Conversely suppose each ${\alpha }_a$ has an inverse ${\alpha }_a^{-1}$. The family ${\beta }_a:={\alpha }_a^{-1}$ is natural: for $f:a⟶b$, $$F(f)\circ {\beta }_a\stackrel{{\beta }_b{\alpha }_b=\mathrm{id}}{=}{\beta }_b\circ {\alpha }_b\circ F(f)\circ {\beta }_a\stackrel{nat.\alpha }{=}{\beta }_b\circ G(f)\circ {\alpha }_a\circ {\beta }_a\stackrel{{\alpha }_a{\beta }_a=\mathrm{id}}{=}{\beta }_b\circ G(f).$$ Then $\beta \circ \alpha$ and $\alpha \circ \beta$ are the identities componentwise. ◻

Such an $\alpha$ is a natural isomorphism, and $F$ and $G$ are naturally isomorphic.

Equivalence of categories

Two categories can agree in everything that is said about arrows and still have different objects. $\mathbf{Ctx}$ has as objects all contexts, under all choices of variable names; a context and its renaming are isomorphic by the renaming substitution and its inverse, and nothing said in terms of arrows distinguishes them. The comparison of $\mathbf{Ctx}$ with its nameless form requires the following notions.

The forgetful functor $U:\mathbf{Mon}\to \mathbf{Set}$ is faithful, because a homomorphism is a function, and not full, because not every function between carriers is a homomorphism. A monotone map $F:P\to Q$ is always faithful, hom-sets having at most one element, and it is full exactly when $F(a)\le F(b)$ implies $a\le b$. The renaming category of example 141.12 is not a full subcategory of $\mathbf{Ctx}$: it has the same objects, but the arrow $(fx)$ of (141.1) is not a renaming.

An isomorphism of categories is a bijection on objects and on each hom-set. An equivalence need not be: it identifies objects only up to isomorphism, which is the identification the arrows can see.

Proof of Theorem 141.46 — Characterization of equivalences

Proof. Only if. Let $G,\eta ,\epsilon$ be as in definition 141.45. Essential surjectivity: for an object $d$, ${\epsilon }_d:F(G(d))⟶d$ is an isomorphism, so $d\cong F(c)$ with $c:=G(d)$. Faithfulness: for $f,f^{\prime }:a⟶b$ with $F(f)=F(f^{\prime })$, naturality of $\eta$ at $f$ reads $G(F(f))\circ {\eta }_a={\eta }_b\circ f$, so The functor $G$ is faithful as well. If $g,g^{\prime }:d⟶d^{\prime }$ and $G(g)=G(g^{\prime })$, naturality of $\epsilon$ gives Fullness: let $g:F(a)⟶F(b)$ and set $f:={\eta }_b^{-1}\circ G(g)\circ {\eta }_a:a⟶b$. Then $$G(F(f))\stackrel{nat.\eta }{=}{\eta }_b\circ f\circ {\eta }_a^{-1}\stackrel{def.f}{=}{\eta }_b\circ {\eta }_b^{-1}\circ G(g)\circ {\eta }_a\circ {\eta }_a^{-1}\stackrel{iso}{=}G(g),$$ and faithfulness of $G$ gives $F(f)=g$.

If. Let $F$ be fully faithful and essentially surjective. The inverse functor is built in four stages.

Objects. By essential surjectivity, choose for each object $d$ of $\mathcal{D}$ an object $G(d)$ of $\mathcal{C}$ and an isomorphism ${\epsilon }_d:F(G(d))⟶d$; this choice is discussed after the proof.

Arrows. For an arrow $g:d⟶d^{\prime }$, the composite ${\epsilon }_{d^{\prime }}^{-1}\circ g\circ {\epsilon }_d$ is an arrow $F(G(d))⟶F(G(d^{\prime }))$, and since $F$ is fully faithful there is exactly one arrow $G(g):G(d)⟶G(d^{\prime })$ with $$F(G(g))={\epsilon }_{d^{\prime }}^{-1}\circ g\circ {\epsilon }_d.$$ $G$ is a functor: $F(G({\mathrm{id}}_d))\stackrel{(141.8)}{=}{\epsilon }_d^{-1}\circ {\epsilon }_d\stackrel{iso}{=}{\mathrm{id}}_{F(G(d))}\stackrel{functor}{=}F({\mathrm{id}}_{G(d)})$, and for $g^{\prime }:d^{\prime }⟶d^{″}$, so faithfulness of $F$ gives the two functor laws.

The counit. Equation (141.8) rearranged, $g\circ {\epsilon }_d={\epsilon }_{d^{\prime }}\circ F(G(g))$, is naturality of $\epsilon :F\circ G\Rightarrow {\mathrm{Id}}_{\mathcal{D}}$, and its components are isomorphisms, so $\epsilon$ is a natural isomorphism by proposition 141.43.

The unit. For each object $c$ of $\mathcal{C}$, ${\epsilon }_{F(c)}:F(G(F(c)))⟶F(c)$ is an isomorphism between two objects in the image of $F$, so by full faithfulness there is exactly one ${\eta }_c:c⟶G(F(c))$ with $F({\eta }_c)={\epsilon }_{F(c)}^{-1}$. It is an isomorphism: for the unique $\theta$ with $F(\theta )={\epsilon }_{F(c)}$, $F(\theta \circ {\eta }_c)={\epsilon }_{F(c)}\circ {\epsilon }_{F(c)}^{-1}=F({\mathrm{id}}_c)$, so $\theta \circ {\eta }_c={\mathrm{id}}_c$ by faithfulness, and likewise ${\eta }_c\circ \theta ={\mathrm{id}}_{G(F(c))}$. Naturality of $\eta$ at $f:c⟶c^{\prime }$ is $G(F(f))\circ {\eta }_c={\eta }_{c^{\prime }}\circ f$; apply $F$ to both sides: and faithfulness of $F$ gives the equation itself. ◻

Proof of Lemma 141.47 — Inverse functors are unique up to natural isomorphism

Proof. For each object $d$ of $\mathcal{D}$, define $${\alpha }_d:=G^{\prime }({\epsilon }_d)\circ {\eta }_{G(d)}^{\prime }:G(d)⟶G^{\prime }(d).$$ Both factors are isomorphisms. For $g:d⟶e$, functoriality, naturality of $\epsilon$, and naturality of ${\eta }^{\prime }$ give Thus $\alpha :G\Rightarrow G^{\prime }$ is natural, and proposition 141.43 makes it a natural isomorphism. ◻

The “if” direction chose one object $G(d)$ and one isomorphism ${\epsilon }_d$ for each $d$. When no rule singles them out, this is a use of the axiom of choice, over a class when the objects of $\mathcal{D}$ do not form a set; and the inverse functor $G$ depends on the choices, two inverse functors from different choices being naturally isomorphic by lemma 141.47. In the case that follows the choice is canonical, a renaming to $x_1,\dots ,x_n$, and no choice principle is used.

Proof of Proposition 141.48 — Named and nameless contexts

Proof. The inclusion of a full subcategory is fully faithful. It is essentially surjective: a context $\mathrm{\Gamma }=y_1:A_1,\dots ,y_n:A_n$ is isomorphic to $X:=x_1:A_1,\dots ,x_n:A_n$ by the renaming $\sigma :=(y_1,\dots ,y_n):\mathrm{\Gamma }⟶X$ and $\tau :=(x_1,\dots ,x_n):X⟶\mathrm{\Gamma }$, since $\tau \circ \sigma =(x_1[\sigma ],\dots ,x_n[\sigma ])=(y_1,\dots ,y_n)={\mathrm{id}}_{\mathrm{\Gamma }}$ and $\sigma \circ \tau =(y_1[\tau ],\dots ,y_n[\tau ])=(x_1,\dots ,x_n)={\mathrm{id}}_X$. So the inclusion is an equivalence by theorem 141.46. It is not an isomorphism of categories: an isomorphism of categories is a bijection on objects, and the context $y:\mathbf{2}$ is not in ${\mathbf{Ctx}}_0$. ◻

An object of ${\mathbf{Ctx}}_0$ is determined by its list of types, so the contexts of ${\mathbf{Ctx}}_0$ are nameless, a variable being its position, while its arrows are still lists of named terms. The proposition is the precise statement that the choice of variable names in a context adds nothing that substitutions can see. An inverse to the inclusion sends each context to its canonical renaming; a different choice of canonical names gives another inverse, naturally isomorphic to it by lemma 141.47.

Representable functors and the Yoneda lemma

A functor $K:\mathcal{C}\to \mathbf{Set}$ assigns to each object $a$ a set of observations $K(a)$, and to each arrow $f:a⟶b$ a way $K(f)$ of transporting observations. The hom-functor ${\mathrm{hom}}_{\mathcal{C}}(r,-)$ of proposition 141.37 is the system whose observations at $a$ are the arrows $r⟶a$, transported by composition. The question this section answers is when an arbitrary $K$ is of this form: when every observation in every $K(a)$ arises, by transport along a unique arrow, from one observation at one test object $r$.

The following calculation shows that $\varphi$ is recovered from $u$ alone, which is why $u$ is called universal. For any natural $\varphi :{\mathrm{hom}}_{\mathcal{C}}(r,-)\Rightarrow K$, any object $a$, and any $f:r⟶a$, So every observation ${\varphi }_a(f)$ is the transport $K(f)(u)$ of the one element $u$, and when $\varphi$ is an isomorphism every element of $K(a)$ is such a transport for exactly one $f$. Calculation (141.9) did not use that $\varphi$ is an isomorphism; it holds for every natural transformation out of a hom-functor, and that is the lemma. One more family is needed to state how the lemma varies with $r$.

Proof of Lemma 141.51 — Precomposition

Proof. At $f:a⟶b$ both composites of (141.7) send $h\in {\mathrm{hom}}_{\mathcal{C}}(r,a)$ to $f\circ h\circ g$, by associativity. ◻

Proof of Theorem 141.52 — Yoneda

Proof. The proof has five parts: $\mathrm{\Psi }(u)$ is natural, $\mathrm{\Phi }\circ \mathrm{\Psi }$ and $\mathrm{\Psi }\circ \mathrm{\Phi }$ are identities, and the two naturality equations hold. The superscript and subscript of $\mathrm{\Phi },\mathrm{\Psi }$ are omitted when fixed.

$\mathrm{\Psi }(u)$ is natural. Fix $u\in K(r)$. The components $\mathrm{\Psi }(u{)}_a:{\mathrm{hom}}_{\mathcal{C}}(r,a)\to K(a)$ are functions. For $f:a⟶b$ and $h\in {\mathrm{hom}}_{\mathcal{C}}(r,a)$, which is (141.7) at $f$.

$\mathrm{\Phi }\circ \mathrm{\Psi }={\mathrm{id}}_{K(r)}$. For $u\in K(r)$, $$\mathrm{\Phi }(\mathrm{\Psi }(u))=\mathrm{\Psi }(u{)}_r({\mathrm{id}}_r)=K({\mathrm{id}}_r)(u)\stackrel{(141.4)}{=}{\mathrm{id}}_{K(r)}(u)=u.$$

$\mathrm{\Psi }\circ \mathrm{\Phi }$ is the identity. For natural $\varphi :{\mathrm{hom}}_{\mathcal{C}}(r,-)\Rightarrow K$, an object $a$, and $f:r⟶a$, $$\mathrm{\Psi }(\mathrm{\Phi }(\varphi ){)}_a(f)=K(f)({\varphi }_r({\mathrm{id}}_r))\stackrel{(141.9)}{=}{\varphi }_a(f),$$ so $\mathrm{\Psi }(\mathrm{\Phi }(\varphi ))$ and $\varphi$ agree at every component and every argument.

Naturality in $K$. For $\alpha :K\Rightarrow K^{\prime }$ and $\varphi :{\mathrm{hom}}_{\mathcal{C}}(r,-)\Rightarrow K$, the composite $\alpha \circ \varphi$ is natural, being a composite of natural transformations, and $${\mathrm{\Phi }}_r^{K^{\prime }}(\alpha \circ \varphi )=(\alpha \circ \varphi {)}_r({\mathrm{id}}_r)={\alpha }_r({\varphi }_r({\mathrm{id}}_r))={\alpha }_r({\mathrm{\Phi }}_r^K(\varphi )).$$

Naturality in $r$. For $g:s⟶r$ and $\psi :{\mathrm{hom}}_{\mathcal{C}}(s,-)\Rightarrow K$, the composite $\psi \circ {\mathrm{hom}}_{\mathcal{C}}(g,-)$ is a natural transformation ${\mathrm{hom}}_{\mathcal{C}}(r,-)\Rightarrow K$ by lemma 141.51, and where (141.9) is applied to $\psi$ at the arrow $g:s⟶r$. ◻

The theorem applies to presheaves through the opposite category. A presheaf $K:{\mathcal{C}}^{\mathrm{op}}\to \mathbf{Set}$ is a functor on ${\mathcal{C}}^{\mathrm{op}}$, and the hom-functor of ${\mathcal{C}}^{\mathrm{op}}$ at $r$ is ${\mathrm{hom}}_{{\mathcal{C}}^{\mathrm{op}}}(r,-)={\mathrm{hom}}_{\mathcal{C}}(-,r)$, the presheaf $a\mapsto {\mathrm{hom}}_{\mathcal{C}}(a,r)$ with $f:a⟶b$ acting by $h\mapsto h\circ f$. Theorem 141.52 for ${\mathcal{C}}^{\mathrm{op}}$ therefore reads:

Proof of Corollary 141.53 — Yoneda for presheaves

Proof. Every arrow and composite in the proof of theorem 141.52 is read in ${\mathcal{C}}^{\mathrm{op}}$; by definition 141.25, an arrow $f:a⟶b$ of ${\mathcal{C}}^{\mathrm{op}}$ is an arrow $b⟶a$ of $\mathcal{C}$ and ${\mathrm{hom}}_{{\mathcal{C}}^{\mathrm{op}}}(r,-)(f)$ is $h\mapsto h\circ f$ in $\mathcal{C}$. No step of that proof used anything about $\mathcal{C}$ beyond (141.2), which hold in ${\mathcal{C}}^{\mathrm{op}}$. ◻

The two naturality equations (141.10) say one thing about a function of two arguments, an object and a functor. To state it as one naturality, form a category of pairs.

The laws hold in each coordinate separately. A bifunctor $F:\mathcal{C}\times \mathcal{D}\to \mathcal{E}$ is a functor in each argument when the other is fixed, since $F(f,{\mathrm{id}}_b)$ and $F({\mathrm{id}}_a,g)$ satisfy (141.4); and the two partial actions commute, $F(f,{\mathrm{id}}_{b^{\prime }})\circ F({\mathrm{id}}_a,g)=F(f,g)=F({\mathrm{id}}_{a^{\prime }},g)\circ F(f,{\mathrm{id}}_b)$, because $(f,{\mathrm{id}}_{b^{\prime }})\circ ({\mathrm{id}}_a,g)=(f,g)=({\mathrm{id}}_{a^{\prime }},g)\circ (f,{\mathrm{id}}_b)$ in $\mathcal{C}\times \mathcal{D}$.

Proof of Proposition 141.55 — The hom bifunctor

Proof. An arrow $(a,b)⟶(a^{\prime },b^{\prime })$ of ${\mathcal{C}}^{\mathrm{op}}\times \mathcal{C}$ is a pair of an arrow $f:a^{\prime }⟶a$ of $\mathcal{C}$ and an arrow $g:b⟶b^{\prime }$, so the typing of ${\mathrm{hom}}_{\mathcal{C}}(f,g)$ is as stated. For a second pair $f^{\prime }:a^{″}⟶a^{\prime }$, $g^{\prime }:b^{\prime }⟶b^{″}$, the composite in ${\mathcal{C}}^{\mathrm{op}}\times \mathcal{C}$ is $(f\circ f^{\prime },g^{\prime }\circ g)$, and identities are preserved by the unit laws. ◻

Fixing $a$ recovers proposition 141.37; fixing $b$ gives the presheaf ${\mathrm{hom}}_{\mathcal{C}}(-,b)$. In $\mathbf{Ctx}$ the bifunctor reads ${\mathrm{hom}}_{\mathbf{Ctx}}(\sigma ,\tau )(\rho )=\tau \circ \rho \circ \sigma$: substitute on both sides.

Proof of Lemma 141.56 — Naturality in each variable

Proof. Joint naturality at $(f,g)$ specializes to the two separate conditions at $(f,{\mathrm{id}}_b)$ and $({\mathrm{id}}_a,g)$. Conversely, since $(f,g)=({\mathrm{id}}_{a^{\prime }},g)\circ (f,{\mathrm{id}}_b)$ in $\mathcal{C}\times \mathcal{D}$,  ◻

Let $\mathcal{C}$ be small, so that $[\mathcal{C},\mathbf{Set}]$ is a category. Define two functors $\mathcal{C}\times [\mathcal{C},\mathbf{Set}]\to \mathbf{Set}$ on objects by $$\mathrm{Ev}(r,K):=K(r),\mathrm{Nt}(r,K):=\mathrm{Nat}({\mathrm{hom}}_{\mathcal{C}}(r,-),K),$$ and on an arrow $(g,\alpha ):(s,K)⟶(r,K^{\prime })$, that is $g:s⟶r$ and $\alpha :K\Rightarrow K^{\prime }$, by

Proof of Proposition 141.57 — Yoneda as a natural isomorphism

Proof. $\mathrm{Ev}({\mathrm{id}}_r,{\mathrm{id}}_K)$ is the identity, and for $(g^{\prime },{\alpha }^{\prime }):(r,K^{\prime })⟶(r^{\prime },K^{″})$ and $u\in K(s)$, $\mathrm{Nt}({\mathrm{id}}_r,{\mathrm{id}}_K)(\psi )=\psi$ because ${\mathrm{hom}}_{\mathcal{C}}({\mathrm{id}}_r,-)$ is the identity transformation, and the composition law is associativity of composition of natural transformations together with ${\mathrm{hom}}_{\mathcal{C}}(g^{\prime }\circ g,-)={\mathrm{hom}}_{\mathcal{C}}(g,-)\circ {\mathrm{hom}}_{\mathcal{C}}(g^{\prime },-)$, both sides sending $h$ to $h\circ g^{\prime }\circ g$. By lemma 141.56, naturality of $\mathrm{\Phi }$ may be checked in each variable separately, and the two conditions are exactly the two equations of (141.10). Each component is a bijection by theorem 141.52, so $\mathrm{\Phi }$ is a natural isomorphism by proposition 141.43. ◻

A presheaf $K$ on $\mathcal{C}$ is representable when $K\cong {\mathrm{hom}}_{\mathcal{C}}(-,r)$ in $[{\mathcal{C}}^{\mathrm{op}},\mathbf{Set}]$ for some object $r$, and its universal element is again ${\varphi }_r({\mathrm{id}}_r)\in K(r)$ for the isomorphism $\varphi$.

The two facts used in proposition 141.29 are representations. The identity functor $\mathrm{Id}:\mathbf{Set}\to \mathbf{Set}$ is represented by $1$ with universal element $\ast \in 1$: by theorem 141.52, $\mathrm{Nat}({\mathrm{hom}}_{\mathbf{Set}}(1,-),\mathrm{Id})\cong \mathrm{Id}(1)=1$, and the component at $A$ of the transformation determined by $\ast$ sends $\underset{―}{x}:1\to A$ to $\mathrm{Id}(\underset{―}{x})(\ast )=x$, the bijection between arrows $1\to A$ and elements of $A$. The presheaf $\mathcal{P}(B):=\{S\mid S\subseteq B\}$, with $\mathcal{P}(f)$ the inverse image along $f$, is represented by $2$ with universal element $\{1\}\subseteq 2$: the transformation determined by $\{1\}$ sends $\chi :B\to 2$ to ${\chi }^{-1}\{1\}$, the bijection between arrows $B\to 2$ and subsets of $B$. In $\mathbf{Ctx}$, the test object $\cdot$ observes environments (proposition 141.36), and proposition 141.60 shows that the test object $⟨A⟩$ observes terms.

That $\mathrm{y}(g)$ is natural and that $\mathrm{y}$ satisfies (141.4) are both associativity: $g\circ (h\circ f)=(g\circ h)\circ f$ gives naturality, and $(g^{\prime }\circ g)\circ h=g^{\prime }\circ (g\circ h)$ gives $\mathrm{y}(g^{\prime }\circ g)=\mathrm{y}(g^{\prime })\circ \mathrm{y}(g)$.

Proof of Corollary 141.59 — The embedding is fully faithful

Proof. Apply corollary 141.53 with $K:=\mathrm{y}(r^{\prime })$: $\mathrm{Nat}(\mathrm{y}(r),\mathrm{y}(r^{\prime }))\cong \mathrm{y}(r^{\prime })(r)={\mathrm{hom}}_{\mathcal{C}}(r,r^{\prime })$, and the inverse $\mathrm{\Psi }$ sends $g$ to the transformation $h\mapsto \mathrm{y}(r^{\prime })(h)(g)=g\circ h$, which is $\mathrm{y}(g)$. For the consequence, let $\varphi :\mathrm{y}(r)\Rightarrow \mathrm{y}(r^{\prime })$ and $\psi :\mathrm{y}(r^{\prime })\Rightarrow \mathrm{y}(r)$ be mutually inverse. By the bijection just proved, $\varphi =\mathrm{y}(g)$ and $\psi =\mathrm{y}(g^{\prime })$ for unique $g:r⟶r^{\prime }$ and $g^{\prime }:r^{\prime }⟶r$, and $$\mathrm{y}(g^{\prime }\circ g)\stackrel{functor}{=}\mathrm{y}(g^{\prime })\circ \mathrm{y}(g)\stackrel{choice}{=}\psi \circ \varphi \stackrel{hyp.}{=}{\mathrm{id}}_{\mathrm{y}(r)}\stackrel{functor}{=}\mathrm{y}({\mathrm{id}}_r),$$ so $g^{\prime }\circ g={\mathrm{id}}_r$ by injectivity of $\mathrm{y}$ on arrows; likewise $g\circ g^{\prime }={\mathrm{id}}_{r^{\prime }}$. ◻

The presheaf of terms is representable, and the representing object is the smallest context that declares a variable of the right type.

Proof of Proposition 141.60 — Terms are represented by one variable

Proof. A substitution $\mathrm{\Gamma }⟶⟨A⟩$ is a one-element list $(e)$ with $\mathrm{\Gamma }⊢e:A$, so ${\varphi }_{\mathrm{\Gamma }}$ is a bijection with inverse $e\mapsto (e)$. Naturality at $\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }$: for $(e)\in {\mathrm{hom}}_{\mathbf{Ctx}}(\mathrm{\Delta },⟨A⟩)$, $${\mathrm{Tm}}_A(\sigma )({\varphi }_{\mathrm{\Delta }}((e)))=e[\sigma ]\stackrel{def.\circ }{=}{\varphi }_{\mathrm{\Gamma }}((e)\circ \sigma )={\varphi }_{\mathrm{\Gamma }}(\mathrm{y}(⟨A⟩)(\sigma )((e))).$$ The universal element is ${\varphi }_{⟨A⟩}({\mathrm{id}}_{⟨A⟩})$, and ${\mathrm{id}}_{⟨A⟩}=(x)$, so it is $x$. ◻

Proof of Theorem 141.61 — Natural operations on terms are substitutions

Proof. By proposition 141.60, ${\mathrm{Tm}}_A\cong \mathrm{y}(⟨A⟩)$, so composing with that isomorphism identifies $\mathrm{Nat}({\mathrm{Tm}}_A,{\mathrm{Tm}}_B)$ with $\mathrm{Nat}(\mathrm{y}(⟨A⟩),{\mathrm{Tm}}_B)$. Corollary 141.53 with $r=⟨A⟩$ and $K={\mathrm{Tm}}_B$ identifies $\mathrm{Nat}(\mathrm{y}(⟨A⟩),{\mathrm{Tm}}_B)$ with ${\mathrm{Tm}}_B(⟨A⟩)$, the terms $x:A⊢b:B$. Tracing the bijections: a term $b$ goes to $\mathrm{\Psi }(b)$, whose component at $\mathrm{\Gamma }$ sends $(e):\mathrm{\Gamma }⟶⟨A⟩$ to ${\mathrm{Tm}}_B((e))(b)=b[(e)]=b[e/x]$; and a natural $\alpha :{\mathrm{Tm}}_A\Rightarrow {\mathrm{Tm}}_B$ goes to $\mathrm{\Phi }(\alpha \circ \varphi )={\alpha }_{⟨A⟩}({\varphi }_{⟨A⟩}({\mathrm{id}}_{⟨A⟩}))={\alpha }_{⟨A⟩}(x)$. ◻

The theorem is the precise form of the slogan that a natural family may use its argument only through substitution-preserving operations. The family $\mathrm{at}$ of exercise 141.8 is the term $xt$; the family $c$ of example 141.40 corresponds to no term, because $c_{⟨\mathbf{2}⟩}(x)=\mathsf{tt}$ would give $c_{\mathrm{\Gamma }}(e)=\mathsf{tt}[e/x]=\mathsf{tt}$ for every $e$, which $c$ does not satisfy.

A context with one more declaration decomposes, as a presheaf, into the shorter context and the terms of the added type.

Proof of Proposition 141.62 — Extension of a context

Proof. A substitution $\mathrm{\Delta }⟶\mathrm{\Gamma },x:A$ is a list of $n+1$ terms whose first $n$ entries form a substitution $\mathrm{\Delta }⟶\mathrm{\Gamma }$ and whose last entry is a term $\mathrm{\Delta }⊢a:A$, so the function is a bijection. Naturality at $\sigma :{\mathrm{\Delta }}^{\prime }⟶\mathrm{\Delta }$: both composites send $(b_1,\dots ,b_n,a)$ to $((b_1[\sigma ],\dots ,b_n[\sigma ]),a[\sigma ])$, by definition 141.4 on the left and componentwise on the right. ◻

Proof of Theorem 141.63 — Natural binary operations are two-variable terms

Proof. Apply proposition 141.62 to the context $x:A$ and the added declaration $x^{\prime }:A^{\prime }$, then apply proposition 141.60 for $A$. The resulting natural isomorphisms give $$\mathrm{y}(x:A,x^{\prime }:A^{\prime })\cong \mathrm{y}(x:A)\times {\mathrm{Tm}}_{A^{\prime }}\cong {\mathrm{Tm}}_A\times {\mathrm{Tm}}_{A^{\prime }}.$$ Yoneda (corollary 141.53) therefore identifies natural transformations from the product to ${\mathrm{Tm}}_B$ with ${\mathrm{Tm}}_B(x:A,x^{\prime }:A^{\prime })$. Tracing the representing substitution sends $(e,e^{\prime })$ to $b[e/x,e^{\prime }/x^{\prime }]$. For $A=A^{\prime }\to B$, the term $x{x}^{\prime }$ has type $B$, and its component is ordinary application. ◻

Representability says that every element of every $K(a)$ is $K(f)(u)$ for exactly one $f:a⟶r$. Collect all the elements of all the $K(a)$ into one structure, with the arrows that transport one to another, and this uniqueness becomes a terminal object. The case $K={\mathrm{Tm}}_A$ shows the structure first. Its elements are the terms in context, the pairs $(\mathrm{\Gamma },e)$ with $\mathrm{\Gamma }⊢e:A$; a substitution $\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }$ transports $(\mathrm{\Delta },e^{\prime })$ to $(\mathrm{\Gamma },e^{\prime }[\sigma ])$, so take as arrows $(\mathrm{\Gamma },e)⟶(\mathrm{\Delta },e^{\prime })$ the substitutions $\sigma :\mathrm{\Gamma }⟶\mathrm{\Delta }$ with $e^{\prime }[\sigma ]=e$. These compose: if also $\tau :\mathrm{\Delta }⟶\mathrm{\Theta }$ with $e^{″}[\tau ]=e^{\prime }$, then $e^{″}[\tau \circ \sigma ]=e^{″}[\tau ][\sigma ]=e$ by lemma 141.5; and ${\mathrm{id}}_{\mathrm{\Gamma }}$ is an arrow $(\mathrm{\Gamma },e)⟶(\mathrm{\Gamma },e)$. The pair $(⟨A⟩,x)$ is terminal: an arrow $(\mathrm{\Gamma },e)⟶(⟨A⟩,x)$ is a substitution $\sigma :\mathrm{\Gamma }⟶⟨A⟩$ with $x[\sigma ]=e$, that is, with $\sigma (x)=e$, and $(e)$ is the only one. Write $\int {\mathrm{Tm}}_A$ for this category. The same recipe applies to any presheaf.

The composite of $f:(a,u)⟶(b,v)$ and $g:(b,v)⟶(c,w)$ is an arrow of $\int K$ because $K(g\circ f)(w)\stackrel{(141.5)}{=}K(f)(K(g)(w))\stackrel{garrow}{=}K(f)(v)\stackrel{farrow}{=}u$, and ${\mathrm{id}}_a$ is one because $K({\mathrm{id}}_a)(u)=u$; the laws are inherited from $\mathcal{C}$. When $\mathcal{C}$ is a preorder $P$, $\int K$ is again a preorder: $(a,u)\le (b,v)$ exactly when $a\le b$ and the restriction of $v$ along $a\le b$ is $u$. The elements of $K$ are stacked over the elements of $P$, each $u\in K(a)$ over its index $a$, and ordered by restriction; the projection forgets the upper layer.

Proof of Proposition 141.65 — Representability by a terminal element

Proof. Let $\varphi :\mathrm{y}(r)\Rightarrow K$ be a natural isomorphism with universal element $u={\varphi }_r({\mathrm{id}}_r)$; by corollary 141.53, $\varphi =\mathrm{\Psi }(u)$, so ${\varphi }_a(f)=K(f)(u)$ for $f:a⟶r$. An arrow $(a,v)⟶(r,u)$ of $\int K$ is an $f:a⟶r$ with $K(f)(u)=v$, that is, with ${\varphi }_a(f)=v$; since ${\varphi }_a$ is a bijection there is exactly one, so $(r,u)$ is terminal. Conversely let $(r,u)$ be terminal. For each $a$ and $v\in K(a)$ there is exactly one $f:a⟶r$ with $K(f)(u)=v$, so $\mathrm{\Psi }(u{)}_a:f\mapsto K(f)(u)$ is a bijection ${\mathrm{hom}}_{\mathcal{C}}(a,r)\to K(a)$; $\mathrm{\Psi }(u)$ is natural by corollary 141.53, hence a natural isomorphism by proposition 141.43, with universal element $\mathrm{\Psi }(u{)}_r({\mathrm{id}}_r)=K({\mathrm{id}}_r)(u)=u$. ◻

For $K={\mathrm{Tm}}_A$ this is proposition 141.60 seen from inside. For the representable $\mathrm{y}(r)={\mathrm{hom}}_{\mathcal{C}}(-,r)$, the objects of $\int \mathrm{y}(r)$ are the arrows $h:a⟶r$ and an arrow $(a,h)⟶(b,h^{\prime })$ is an $f:a⟶b$ with $h^{\prime }\circ f=h$: the arrows into $r$ with the factorizations between them. This category is called the slice of $\mathcal{C}$ over $r$ and written $\mathcal{C}/r$.

The chapter began with three composition structures proved one at a time. Two of them are objects of one kind: $\mathbf{Ctx}$ is a category, and the semantic values of chapter 49 form a presheaf on its preorder of extensions. The restriction lemma of that chapter, which states that evaluating a term and then restricting the value equals restricting the environment and then evaluating, is the statement that evaluation is a natural transformation between two presheaves on that preorder. That is the statement of agreement which the three repeated proofs could not express: two composition structures agree when a family of maps between them is natural. What theorem 141.61 does for one variable, theorem 141.63 does for two; the contexts that represent families of terms whose types depend on earlier variables belong to the later treatment of dependent categorical semantics.

Bibliographic notes.

Categories, functors, and natural transformations were introduced by Eilenberg and Mac Lane [EML45], who defined categories in order to define naturality. The lemma of section 141.9 is named for Yoneda; Mac Lane [ML98a] records its origin in a conversation with him in 1954, and proves the characterization of equivalences, theorem 141.46, as his Theorem IV.4.1. The treatment of monomorphisms and epimorphisms by test objects, and the example of proposition 141.31, follow Asperti and Longo [AL91], whose book develops category theory from typed lambda calculi. The representability of the presheaf of terms by a one-variable context, proposition 141.60, is the elementary case of the representable natural transformations that Awodey uses to define natural models of dependent type theory [Awo18].