Def CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso

Modification history

2025-04-15 10:53
Mathlib/CategoryTheory/Yoneda.lean
feat (Yoneda): (co)representing objects are unique up to iso (#24059) …
Added CategoryTheory.Functor.CorepresentableBy.uniqueUpToIsoView on Github →