Theorem CategoryTheory.Equivalence.mkHom_id_inverse

Modification history