Theorem CategoryTheory.Equivalence.mkHom_id_functor

Modification history