Theorems · Definition · category theory

CategoryTheory.Bicategory.Equivalence.recOn

{B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {motive : CategoryTheory.Bicategory.Equivalence a b → Sort u} →
        (t : CategoryTheory.Bicategory.Equivalence a b) →
          ((hom : a ⟶ b) →
              (inv : b ⟶ a) →
                (unit : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp hom inv) →
                  (counit : CategoryTheory.CategoryStruct.comp inv hom ≅ CategoryTheory.CategoryStruct.id b) →
                    (left_triangle :
                        CategoryTheory.Bicategory.leftZigzagIso unit counit =
                          CategoryTheory.Bicategory.leftUnitor hom ≪≫
                            (CategoryTheory.Bicategory.rightUnitor hom).symm) →
                      motive
                        { hom := hom, inv := inv, unit := unit, counit := counit, left_triangle := left_triangle }) →
            motive t

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Cited by

0 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Bicategory