Skip to content

Commit

Permalink
yoneda lemma section title
Browse files Browse the repository at this point in the history
  • Loading branch information
emilyriehl committed Jun 25, 2024
1 parent e905056 commit b032281
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/simplicial-hott/13-yoneda-geodesic.rzk.md
Original file line number Diff line number Diff line change
Expand Up @@ -447,6 +447,8 @@ naturality-covariant-fiberwise-transformation* naturality is automatic.
A is-pre-∞-category-A a b x y f v ϕ)
```

## The Yoneda lemma

For any pre-∞-category $A$ terms $a b : A$, the contravariant Yoneda lemma
provides an equivalence between the type`#!rzk (z : A) → Hom A z a → Hom A z b`
of natural transformations and the type `#!rzk Hom A a b`.
Expand Down

0 comments on commit b032281

Please sign in to comment.