Def CategoryTheory.Functor.CorepresentableBy.toIso

Modification history

2024-10-04 10:12

Mathlib/CategoryTheory/Yoneda.lean

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

Added CategoryTheory.Functor.CorepresentableBy.toIso View on Github →