Theorem CategoryTheory.Bicategory.Equivalence.left_triangle_hom

Modification history

2024-02-10 12:15
Mathlib/CategoryTheory/Bicategory/Adjunction.lean
feat(Bicategory/Adjunction): the left triangle implies the right triangle for equivalences (#10398)
Added CategoryTheory.Bicategory.Equivalence.left_triangle_homView on Github →