Commit 2024-02-10 12:15 ba309fb0

View on Github →

feat(Bicategory/Adjunction): the left triangle implies the right triangle for equivalences (#10398)

Estimated changes

Modified Mathlib/CategoryTheory/Bicategory/Adjunction.lean

added theorem CategoryTheory.Bicategory.Equivalence.left_triangle_hom

added theorem CategoryTheory.Bicategory.Equivalence.right_triangle

added theorem CategoryTheory.Bicategory.Equivalence.right_triangle_hom

added theorem CategoryTheory.Bicategory.rightZigzag_idempotent_of_left_triangle

added theorem CategoryTheory.Bicategory.right_triangle_of_left_triangle