Theorems · Theorem · category theory

CategoryTheory.Bicategory.Equivalence.left_triangle_hom

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} (e : CategoryTheory.Bicategory.Equivalence a b),
  CategoryTheory.Bicategory.leftZigzag e.unit.hom e.counit.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor e.hom).hom
      (CategoryTheory.Bicategory.rightUnitor e.hom).inv

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory