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 of above is equivalent to the space of all local sections at of . In analogy with natural transformations from category theory we make the following definition:
Definition. If and are dependent types over , we define
of which the terms are called dependent transformations. We will say that a transformation is an equivalence if is an equivalence for each .
The case where is the dependent space over with for some fixed in is of special importance. We will denote this dependent type by to emphasize on the similarity of the role it plays to the Yoneda embedding of in the category of presheaves over . Indeed, we will soon be able to prove that . We call a transformation from to also a local section of at .
Example. If is a path in , then there is the transformation defined by . So sends for each the paths to the concatenation .
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 and are dependent types over and that is a transformation from to . Then the diagram
commutes up to homotopy for every path in . Here, denotes transportation along with respect to the dependent type . We define when and .
Proof. Let be the type . Since it follows that is inhabited by the canonical term . The assertion follows now by the induction principle for identity types.
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 over and any there is an equivalence
for each and . The equivalences are natural in the sense that the diagram
commutes for every and .
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 for a presheaf on a category and a natural transformation . But as I wrote this blog post, the following short proof occured to me:
Proof. Note that if is inhabited, then is equivalent to . Hence we have
In the last equivalence, we used that is contractible.
By looking at what each of the equivalences does, it is not so hard to see that the equivalence is the map
Following the above commutative square from the top right first to the left and then downwards, we get for a transformation , a path and a transformation , we get the term
Going first downwards and then to the left we get the term . Induction on reveals that there is a path between the two.
Corollary. Taking for we get the equivalence .
Loosely speaking, every function which takes and to a path from to is itself a path from to . Using the Yoneda lemma, we can derive three basic adjunctions from presheaf theory:
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 and let be the function from to given by substitution along , i.e. for . We may also define the function given by
Remark. Consider the projection . Then
We have used that the space is contractible. What this shows is that is equivalent to our original dependent sum when is a projection.
Lemma. For all and we have the equivalence
Proof. We use the Yoneda lemma:
Definition. Suppose that is a function. Define the function given by
Remark. Again, we may consider the map to verify that .
Thus, generalizes the original dependent product construction.
Lemma. For all and we have the equivalence
Proof. In a similar calculation as before, we derive
Definition. We may define the dependent type over by
The product of two dependent types over is defined pointwise as .
Lemma. For any triple , and of dependent types over there is an equivalence
Proof. Note that if there is a path from to , then the spaces and are equivalent. Thus we can make the following calculation proving the assertion:
Remark. That the categorical definition of exponentiation doesn’t fail is no surprise. But actually we could get exponentiation easier by defining to be the dependent type over given by . The correspondence
is then immediate. By taking to be and using the Yoneda lemma, we get
Hence the dependent types and are equivalent, which comes down to the fact that we could have gotten away with the naive approach regarding exponentiation.
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.
Indeed — nice post Egbert!