Theorem CategoryTheory.isRepresentable_of_natIso

Modification history

2026-03-08 20:06

Mathlib/CategoryTheory/Yoneda.lean

chore(CategoryTheory/ShrinkYoneda): `shrinkYoneda.obj X` is representable (#36292)

Modified CategoryTheory.isRepresentable_of_natIso View on Github →

2024-10-04 10:12

Mathlib/CategoryTheory/Yoneda.lean

refactor(CategoryTheory): generalize universes for representable functors (#17389) …

Added CategoryTheory.isRepresentable_of_natIso View on Github →