Theorems · Definition · category theory

CategoryTheory.Bicategory.Equivalence.mk.noConfusion

{B : Type u₁} →
  {inst : CategoryTheory.Bicategory B} →
    {a b : B} →
      {P : Sort u} →
        {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 :
                    autoParam
                      (CategoryTheory.Bicategory.leftZigzagIso unit counit =
                        CategoryTheory.Bicategory.leftUnitor hom ≪≫ (CategoryTheory.Bicategory.rightUnitor hom).symm)
                      CategoryTheory.Bicategory.Equivalence.left_triangle._autoParam} →
                  {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' :
                              autoParam
                                (CategoryTheory.Bicategory.leftZigzagIso unit' counit' =
                                  CategoryTheory.Bicategory.leftUnitor hom' ≪≫
                                    (CategoryTheory.Bicategory.rightUnitor hom').symm)
                                CategoryTheory.Bicategory.Equivalence.left_triangle._autoParam} →
                            { hom := hom, inv := inv, unit := unit, counit := counit, left_triangle := left_triangle } =
                                { hom := hom', inv := inv', unit := unit', counit := counit',
                                  left_triangle := left_triangle' } →
                              (hom ≍ hom' → inv ≍ inv' → unit ≍ unit' → counit ≍ counit' → P) → P

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Cited by

1 results in Mathlib

Foundations

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