Theorems · Theorem · category theory

CategoryTheory.Bicategory.Adjunction.mk.injEq

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (unit : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g)
  (counit : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b)
  (left_triangle :
    autoParam
      (CategoryTheory.Bicategory.leftZigzag unit counit =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
          (CategoryTheory.Bicategory.rightUnitor f).inv)
      CategoryTheory.Bicategory.Adjunction.left_triangle._autoParam)
  (right_triangle :
    autoParam
      (CategoryTheory.Bicategory.rightZigzag unit counit =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
          (CategoryTheory.Bicategory.leftUnitor g).inv)
      CategoryTheory.Bicategory.Adjunction.right_triangle._autoParam)
  (unit_1 : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g)
  (counit_1 : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b)
  (left_triangle_1 :
    autoParam
      (CategoryTheory.Bicategory.leftZigzag unit_1 counit_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
          (CategoryTheory.Bicategory.rightUnitor f).inv)
      CategoryTheory.Bicategory.Adjunction.left_triangle._autoParam)
  (right_triangle_1 :
    autoParam
      (CategoryTheory.Bicategory.rightZigzag unit_1 counit_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
          (CategoryTheory.Bicategory.leftUnitor g).inv)
      CategoryTheory.Bicategory.Adjunction.right_triangle._autoParam),
  ({ unit := unit, counit := counit, left_triangle := left_triangle, right_triangle := right_triangle } =
      { unit := unit_1, counit := counit_1, left_triangle := left_triangle_1, right_triangle := right_triangle_1 }) =
    (unit = unit_1 ∧ counit = counit_1)

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory