Def CategoryTheory.Functor.RepresentableBy.ofIso

Modification history

2024-10-04 10:12

Mathlib/CategoryTheory/Yoneda.lean

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

Added CategoryTheory.Functor.RepresentableBy.ofIso View on Github →