Skip to content

Other Yoneda formalizations

Below is an incomplete list of Yoneda lemma formalizations in different systems:

Library System Foundations Yoneda
agda-categories Agda Traditional, proof relevant 1-categories1
agda-unimath Agda HoTT/UF 1-categories
UniMath Coq HoTT/UF 1-categories, bicategories2
1lab Cubical Agda HoTT/UF (cubical) 1-categories
mathlib Lean 4 Traditional 1-categories
sinhp/CovariantYonedaLean3 Lean 3 Traditional 1-categories
sinhp/CovariantYonedaLean4 Lean 4 Traditional 1-categories
Archive of Formal Proofs Isabelle/HOL Traditional 1-categories3 4 5
This project Rzk HoTT/UF (simplicial) ∞-categories

  1. The agda-categories library internalizes a version of Hom-equality to each category, resulting in a flavour of bicategory theory. ↩

  2. B. Ahrens, D. Frumin, M. Maggesi, N. Veltri, and N. van der Weide. Bicategories in univalent foundations. Mathematical Structures in Computer Science, vol. 31, no. 10, pp. 1232–1269, 2021. https://arxiv.org/abs/1903.01152 ↩

  3. https://www.isa-afp.org/sessions/category/#Yoneda ↩

  4. https://www.isa-afp.org/sessions/category2/#Yoneda ↩

  5. https://www.isa-afp.org/sessions/category3/#Yoneda ↩