Commit 2025-04-15 10:53 07e34201

View on Github →

feat (Yoneda): (co)representing objects are unique up to iso (#24059)

  • Add isomorphisms that witness the uniqueness of (co)representing objects of a given functor
  • Add isomorphisms that witness the isomorphism of any given (co)representing object to (co)reprX
  • Add Coyoneda.ext to match Yoneda.ext (used in the constructions above).

Estimated changes