From 01a52f934a3a3f548dc2451659382026093a3b55 Mon Sep 17 00:00:00 2001 From: Emily Riehl Date: Mon, 12 Feb 2024 15:33:14 -0500 Subject: [PATCH] mentioned the paper --- README.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README.md b/README.md index 3750d73..a133724 100644 --- a/README.md +++ b/README.md @@ -45,6 +45,9 @@ 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 @@ -61,3 +64,5 @@ rzk typecheck [^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 + +[^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