Theorem CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_hom

Modification history