Theorem CategoryTheory.equiv_punit_iff_unique

Modification history