A type theoretical Yoneda lemma

In this blog post I would like to approach dependendent types from a presheaf point of view. This allows us to take the theory of presheaves as an inspiration for results in homotopy type theory. The first result from this direction is a type theoretical variant of the Yoneda lemma, stating that the fiber $P(a)$ of $P$ above $a$ is equivalent to the space of all local sections at $a$ of $P$ . In analogy with natural transformations from category theory we make the following definition:

Definition. If $P$ and $Q$ are dependent types over $A$ , we define

$\mathsf{hom}(P,Q):=\prod(x:A),\ P(x)\to Q(x)$

of which the terms are called dependent transformations. We will say that a transformation $\sigma:\mathsf{hom}(P,Q)$ is an equivalence if $\sigma(x):P(x)\to Q(x)$ is an equivalence for each $x:A$ .

The case where $P$ is the dependent space over $A$ with $P(x)=x\leadsto a$ for some fixed $a$ in $A$ is of special importance. We will denote this dependent type by $\mathscr{Y}(a)$ to emphasize on the similarity of the role it plays to the Yoneda embedding of $a$ in the category of presheaves over $A$ . Indeed, we will soon be able to prove that $P(a)\simeq\mathsf{hom}(\mathscr{Y}(a),P)$ . We call a transformation from $\mathscr{Y}(a)$ to $P$ also a local section of $P$ at $a$ .

Example. If $p:a\leadsto a^\prime$ is a path in $A$ , then there is the transformation $\mathscr{Y}(p):\mathsf{hom}(\mathscr{Y}(a),\mathscr{Y}(a^\prime))$ defined by $\lambda x.\lambda q.p\bullet q$ . So $\mathscr{Y}(p)$ sends for each $x:A$ the paths $q:x\leadsto a$ to the concatenation $p\bullet q$ .

Note that we didn’t require the naturality in our definition of transformations. This is, however, something that we get for free:

Lemma. Suppose that $P$ and $Q$ are dependent types over $A$ and that $\tau:\mathsf{hom}(P,Q)$ is a transformation from $P$ to $Q$ . Then the diagram

yoneda-diagram-01.pdf

commutes up to homotopy for every path $p:x\leadsto y$ in $A$ . Here, $P(p)$ denotes transportation along $p$ with respect to the dependent type $P$ . We define $\tau(p):=Q(p)\circ\tau(x)$ when $p:x\leadsto y$ and $\tau:\mathsf{hom}(P,Q)$ .

Proof. Let $D(x,y,p)$ be the type $Q(p)\circ\sigma(x)\leadsto\sigma(y)\circ P(p)$ . Since $P(\mathrm{id}_{x})=\mathrm{id}_{P(x)}$ it follows that $D(x,x,\mathrm{id}_{x})$ is inhabited by the canonical term $d(x):=\mathrm{id}_{\sigma(x)}$ . The assertion follows now by the induction principle for identity types.
QED.

Transformations of dependent types may be composed and just as in the case with natural transformations this is done pointwise.

Lemma (Yoneda lemma for dependent types). Assuming function extensionality we have: for any dependent type $P$ over $A$ and any $a:A$ there is an equivalence

$\alpha_{P,a}:P(a)\simeq\mathsf{hom}(\mathscr{Y}(a),P)$

for each $a:A$ and $P:A\to\mathsf{Type}$ . The equivalences $\alpha_{P,a}$ are natural in the sense that the diagram

yoneda-diagram-02.pdf

commutes for every $p:a\leadsto a^\prime$ and $\tau:\mathsf{hom}(P,P^\prime)$ .

Originally, I had a two page long proof featuring some type theoretical relatives of the key ideas of the proof of the categorical Yoneda lemma, like considering $\tau_a(\mathrm{id}_a)\in P(a)$ for a presheaf $P$ on a category $\mathcal{C}$ and a natural transformation $\tau:\mathscr{Y}(a)\Rightarrow P$ . But as I wrote this blog post, the following short proof occured to me:

Proof. Note that if $x\leadsto a$ is inhabited, then $P(x)$ is equivalent to $P(a)$ . Hence we have

$\mathsf{hom}(\mathscr{Y}(a),P)$
$= \prod(x:A),\ (x\leadsto a)\to P(x)$
$\simeq \prod(x:A),\ (x\leadsto a)\to P(a)$
$\simeq \big(\sum(x:A),\ x\leadsto a\big)\to P(a)$
$\simeq P(a).$

In the last equivalence, we used that $\sum(x:A),\ x\leadsto a$ is contractible.

By looking at what each of the equivalences does, it is not so hard to see that the equivalence $\mathsf{hom}(\mathscr{Y}(a),P)\simeq P(a)$ is the map

$\lambda\tau.\tau(a,\mathrm{id}_a)$ .

Following the above commutative square from the top right first to the left and then downwards, we get for a transformation $\tau:\mathsf{hom}(\mathscr{Y}(a),P)$ , a path $p:a^\prime\leadsto a$ and a transformation $\sigma:\mathsf{hom}(P,P^\prime)$ , we get the term

$P^\prime(p)(\sigma(a)(\tau(a,\mathrm{id}_a)))$ of $P^\prime(a^\prime)$ .

Going first downwards and then to the left we get the term $\sigma(a^\prime)(\tau(a^\prime,p))$ . Induction on $p$ reveals that there is a path between the two.
QED.

Corollary. Taking $\mathscr{Y}(b)$ for $P$ we get the equivalence $\mathsf{hom}(\mathscr{Y}(a),\mathscr{Y}(b))\simeq a\leadsto b$ .

Loosely speaking, every function which takes $x:A$ and $p:x\leadsto a$ to a path from $x$ to $b$ is itself a path from $a$ to $b$ . Using the Yoneda lemma, we can derive three basic adjunctions from presheaf theory:

$\exists_f\vdash f^\ast$
$f^\ast\vdash\forall_f$
$(-)\times P\vdash (-)^P$

We will use the remainder of this post to state and prove them. Hopefully, we can distill a good notion of adjunction in the discussion thread below.

Definition. Suppose that $f:A\to B$ and let $f^\ast$ be the function from $(B\to\mathsf{Type})$ to $(A\to\mathsf{Type})$ given by substitution along $f$ , i.e. $f^\ast(Q)(a)=Q(f(a))$ for $Q:B\to A$ . We may also define the function $\exists_f:(A\to\mathsf{Type})\to(B\to\mathsf{Type})$ given by

$\exists_f(P)(b)=\sum(x:A),\ (f(x)\leadsto b)\times P(x).$

Remark. Consider the projection $\mathsf{proj_1}:B\times Y\to B$ . Then

$\exists_{\mathsf{proj_1}}(P)(b)$
$=\sum(\langle b^\prime,y\rangle:B\times Y),\ (b^\prime\leadsto b)\times P(b^\prime,y)$
$\simeq \sum(b^\prime:B)(y:Y),\ (b^\prime\leadsto b)\times P(b,y)$
$\simeq \sum(y:Y),\ P(b,y)\times \left(\sum(b^\prime :B),\ b^\prime\leadsto b\right)$
$\simeq \sum(y:Y),\ P(\langle b,y\rangle).$

We have used that the space $\sum(b^\prime:B),\ b^\prime\leadsto b$ is contractible. What this shows is that $\exists_f$ is equivalent to our original dependent sum when $f$ is a projection.

Lemma. For all $P:A\to\mathsf{Type}$ and $Q:B\to\mathsf{Type}$ we have the equivalence

$\mathsf{hom}(\exists_f(P),Q)\simeq\mathsf{hom}(P,f^\ast(Q)).$

Proof. We use the Yoneda lemma:

$\mathsf{hom}(\exists_f(P),Q)$
$= \prod(b:B),\ \left(\sum(a:A),\ (f(a)\leadsto b)\times P(a)\right)\to Q(b)$
$\simeq \prod(b:B)(a:A),\ ((f(a)\leadsto b)\times P(a))\to Q(b)$
$\simeq \prod(a:A),\ P(a)\to\prod(b:B),\ (b\leadsto f(a))\to Q(b)$
$\simeq \prod(a:A),\ P(a)\to Q(f(a))$
$= \mathsf{hom}(P,f^\ast(Q)).$
QED.

Definition. Suppose that $f:A\to B$ is a function. Define the function $\forall_f:(A\to\mathsf{Type})\to(B\to\mathsf{Type})$ given by

$\forall_f(P)(b)=\prod(a:A),\ (f(a)\leadsto b)\to P(a).$

Remark. Again, we may consider the map $\mathsf{proj_1}:B\times Y\to B$ to verify that $\forall_\mathsf{proj_1} (P)(b)\simeq\prod(y:Y),\ P(b,y)$ .

$\forall_\mathsf{proj_1}(P)(b)$
$=\prod(\langle b^\prime,y\rangle:B\times Y),\ (b^\prime\leadsto b)\to P(b^\prime,y)$
$\simeq \prod(b^\prime:B)(y:Y),\ (b^\prime\leadsto b)\to P(b,y)$
$\simeq \left(\sum(b^\prime:B),\ b^\prime\leadsto b\right)\to \prod(y:Y),\ P(b,y)$
$\simeq \prod(y:Y),\ P(b,y).$

Thus, $\forall_f$ generalizes the original dependent product construction.

Lemma. For all $P:A\to\mathsf{Type}$ and $Q:B\to\mathsf{Type}$ we have the equivalence

$\mathsf{hom}(f^\ast(Q),P)\simeq\mathsf{hom}(Q,\forall_f(P)).$

Proof. In a similar calculation as before, we derive

$\mathsf{hom}(Q,\forall_f(P))$
$=\prod(b:B),\ Q(b)\to\prod(a:A),\ (f(a)\leadsto b)\to P(a)$
$\simeq \prod(a:A)(b:B),\ Q(b)\to(f(a)\leadsto b)\to P(a)$
$\simeq \prod(a:A),\ \big(\sum(b:B),\ Q(b)\times (f(a)\leadsto b)\big)\to P(a)$
$\simeq \prod(a:A),\ \big(\sum(b:B),\ Q(f(a))\times (f(a)\leadsto b)\big)\to P(a)$
$\simeq \prod(a:A),\ Q(f(a))\times\big(\sum(b:B),\ f(a)\leadsto b)\big)\to P(a)$
$\simeq \prod(a:A),\ Q(f(a))\to P(a)$
$= \mathsf{hom}(f^\ast(Q),P)$
QED.

Definition. We may define the dependent type $Q^P$ over $A$ by

$Q^P(a)=\mathsf{hom}(\mathscr{Y}(a)\times P,Q)$

The product $P^\prime\times P$ of two dependent types over $A$ is defined pointwise as $(P^\prime\times P)(a)=P^\prime(a)\times P(a)$ .

Lemma. For any triple $P$ , $Q$ and $R$ of dependent types over $A$ there is an equivalence

$\mathsf{hom}(R,Q^P)\simeq\mathsf{hom}(R\times P,Q).$

Proof. Note that if there is a path from $y$ to $x$ , then the spaces $P(y)$ and $P(x)$ are equivalent. Thus we can make the following calculation proving the assertion:

$\mathsf{hom}(R,Q^P)$
$= \prod(x:A),\ R(x)\to\mathsf{hom}(\mathscr{Y}(x)\times P,Q)$
$= \prod(x:A),\ R(x)\to\left(\prod(y:A),\ (y\leadsto x)\times P(y)\to Q(y)\right)$
$\simeq \prod(x:A),\ R(x)\to\left(\prod (y:A),\ (y\leadsto x)\times P(x)\to Q(y)\right)$
$\simeq \prod(x:A),\ R(x)\to P(x)\to \left(\prod(y:A),\ (y\leadsto x)\to Q(y)\right)$
$\simeq \prod(x:A),\ R(x)\times P(x)\to Q(x)$
$= \mathsf{hom}(R\times P,Q).$
QED.

Remark. That the categorical definition of exponentiation doesn’t fail is no surprise. But actually we could get exponentiation easier by defining $P\to Q$ to be the dependent type over $A$ given by $(P\to Q)(a):=P(a)\to Q(a)$ . The correspondence

$\mathsf{hom}(R,P\to Q)\simeq\mathsf{hom}(R\times P,Q)$

is then immediate. By taking $R$ to be $\mathscr{Y}(a)$ and using the Yoneda lemma, we get

$(P\to Q)(a)\simeq\mathsf{hom}(\mathscr{Y}(a),P\to Q)\simeq\mathsf{hom}(\mathscr{Y}(a)\times P,Q)=Q^P(a).$

Hence the dependent types $P\to Q$ and $Q^P$ are equivalent, which comes down to the fact that we could have gotten away with the naive approach regarding exponentiation.

2 Responses to A type theoretical Yoneda lemma

andrejbauer says:

3 May 2012 at 03:46

Perhaps I should introduce Egbert. He is a masters student at the Utrecht University, on an exchange visit in at the University of Ljubljana. He is working on HoTT topics, as is obvious from this post. Welcome, Egbert.

Steve Awodey says:

5 May 2012 at 00:37

Indeed — nice post Egbert!