Skip to content

Commit

Permalink
fixed spacing in markdown
Browse files Browse the repository at this point in the history
  • Loading branch information
emilyriehl committed Oct 16, 2024
1 parent af87028 commit bc815e3
Showing 1 changed file with 6 additions and 3 deletions.
9 changes: 6 additions & 3 deletions src/simplicial-hott/13-yoneda-geodesic.rzk.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
# A self contained proof of the Yoneda lemma

This file — which is independent of the rest of the simplicial HoTT repository but references a few HoTT preliminaries —
contains a self-contained proof of the ∞-categorical Yoneda lemma in the
This file — which is independent of the rest of the simplicial HoTT
repository but references a few HoTT preliminaries — contains a
self-contained proof of the ∞-categorical Yoneda lemma in the
special case where both functors are contravariantly representable. This is
intended for expository purposes.

Expand All @@ -22,7 +23,9 @@ This is a literate `rzk` file:

The definitions and proofs reference standard concepts from homotopy type theory
including a universe of types denoted `#!rzk U`, the notion of contractible
types, and the notion of equivalence between types. The universe is built into `rzk`, while the homotopy type theory predicates `#!rzk is-contr` and `#!rzk is-equiv` can be found in the HoTT folder of this repository.
types, and the notion of equivalence between types. The universe is built into
`rzk`, while the homotopy type theory predicates `#!rzk is-contr` and
`#!rzk is-equiv` can be found in the HoTT folder of this repository.

Some of the definitions in this file rely on function extensionality:

Expand Down

0 comments on commit bc815e3

Please sign in to comment.