diff --git a/README.md b/README.md
index a133724..22543cf 100644
--- a/README.md
+++ b/README.md
@@ -1,12 +1,12 @@
# Yoneda for ∞-categories
-
+
[](https://github.com/emilyriehl/yoneda/actions/workflows/rzk.yml)
[](https://github.com/emilyriehl/yoneda/actions/workflows/mkdocs.yml)
-> :warning: This project has been __❄ frozen ❄__.
-> For ongoing simplicial HoTT formalization see .
+> :warning: This project has been **❄ frozen ❄**. For ongoing simplicial HoTT
+> formalization see .
This is a formalization library for simplicial Homotopy Type Theory (sHoTT) with
the aim of proving the Yoneda lemma for ∞-categories following the paper
@@ -45,7 +45,10 @@ condition is not required for this result. By analogy, precategories are the
non-univalent 1-categories in HoTT. See also
[other Yoneda formalizations](other.md).
-We presented this work at [CPP 2024](https://popl24.sigplan.org/home/CPP-2024) and published an overview of our formalization project in the conference proceedings as "[Formalizing the ∞-Categorical Yoneda Lemma](https://dl.acm.org/doi/10.1145/3636501.3636945)"
+We presented this work at [CPP 2024](https://popl24.sigplan.org/home/CPP-2024)
+and published an overview of our formalization project in the conference
+proceedings as
+"[Formalizing the ∞-Categorical Yoneda Lemma](https://dl.acm.org/doi/10.1145/3636501.3636945)"
[^3]. This project has been frozen to match its state as of that publication.
## Checking the Formalisations Locally
@@ -58,11 +61,17 @@ We presented this work at [CPP 2024](https://popl24.sigplan.org/home/CPP-2024) a
rzk typecheck
```
-[^1]: Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories.
- Higher Structures 1(1), 147-224. 2017. https://arxiv.org/abs/1705.07442
+[^1]:
+ Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories.
+ Higher Structures 1(1), 147-224. 2017.
-[^2]: Emily Riehl. Could ∞-category theory be taught to undergraduates? Notices of
- the AMS. May 2023.
- https://www.ams.org/journals/notices/202305/noti2692/noti2692.html
+[^2]:
+ Emily Riehl. Could ∞-category theory be taught to undergraduates? Notices of
+ the AMS. May 2023.
+
-[^3]: Nikolai Kudasov, Emily Riehl, Jonathan Weinberger, Formalizing the ∞-Categorical Yoneda Lemma. CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and ProofsJanuary 2024Pages 274–290. https://dl.acm.org/doi/10.1145/3636501.3636945
\ No newline at end of file
+[^3]:
+ Nikolai Kudasov, Emily Riehl, Jonathan Weinberger. Formalizing the
+ ∞-Categorical Yoneda Lemma. CPP 2024: Proceedings of the 13th ACM SIGPLAN
+ International Conference on Certified Programs and ProofsJanuary 2024Pages
+ 274–290.
diff --git a/src/index.md b/src/index.md
index 2f36440..226eadb 100644
--- a/src/index.md
+++ b/src/index.md
@@ -40,6 +40,12 @@ condition is not required for this result. By analogy, precategories are the
non-univalent 1-categories in HoTT. See also
[other Yoneda formalizations](other.md).
+We presented this work at [CPP 2024](https://popl24.sigplan.org/home/CPP-2024)
+and published an overview of our formalization project in the conference
+proceedings as
+"[Formalizing the ∞-Categorical Yoneda Lemma](https://dl.acm.org/doi/10.1145/3636501.3636945)"
+[^3]. This project has been frozen to match its state as of that publication.
+
## Checking the Formalisations Locally
[Install](https://rzk-lang.github.io/rzk/latest/getting-started/install/) the
@@ -58,3 +64,9 @@ rzk typecheck
Emily Riehl. Could ∞-category theory be taught to undergraduates? Notices of
the AMS. May 2023.
+
+[^3]:
+ Nikolai Kudasov, Emily Riehl, Jonathan Weinberger. Formalizing the
+ ∞-Categorical Yoneda Lemma. CPP 2024: Proceedings of the 13th ACM SIGPLAN
+ International Conference on Certified Programs and ProofsJanuary 2024Pages
+ 274–290.