Theorems · Theorem · category theory

CategoryTheory.Bicategory.Adjunction.mk.congr_simp

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

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory