Theorem CategoryTheory.Bicategory.rightUnitor_comp_inv

Modification history