Theorems · Theorem · category theory

CategoryTheory.Bicategory.Equivalence.mk.inj

∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {a b : 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 :
    autoParam
      (CategoryTheory.Bicategory.leftZigzagIso unit counit =
        CategoryTheory.Bicategory.leftUnitor hom ≪≫ (CategoryTheory.Bicategory.rightUnitor hom).symm)
      CategoryTheory.Bicategory.Equivalence.left_triangle._autoParam}
  {hom_1 : a ⟶ b} {inv_1 : b ⟶ a}
  {unit_1 : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp hom_1 inv_1}
  {counit_1 : CategoryTheory.CategoryStruct.comp inv_1 hom_1 ≅ CategoryTheory.CategoryStruct.id b}
  {left_triangle_1 :
    autoParam
      (CategoryTheory.Bicategory.leftZigzagIso unit_1 counit_1 =
        CategoryTheory.Bicategory.leftUnitor hom_1 ≪≫ (CategoryTheory.Bicategory.rightUnitor hom_1).symm)
      CategoryTheory.Bicategory.Equivalence.left_triangle._autoParam},
  { hom := hom, inv := inv, unit := unit, counit := counit, left_triangle := left_triangle } =
      { hom := hom_1, inv := inv_1, unit := unit_1, counit := counit_1, left_triangle := left_triangle_1 } →
    hom = hom_1 ∧ inv = inv_1 ∧ unit ≍ unit_1 ∧ counit ≍ counit_1

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Cited by

1 results in Mathlib

Foundations

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