comp_left_triangle_aux — Mathlib

Lean4
theorem comp_left_triangle_aux (adj₁ : f₁ ⊣ g₁) (adj₂ : f₂ ⊣ g₂) :
    leftZigzag (compUnit adj₁ adj₂) (compCounit adj₁ adj₂) = (λ_ _).hom ≫ (ρ_ _).inv := by
  calc
    _ =
        𝟙 _ ⊗≫
          adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
            f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 _ :=
      by dsimp only [compUnit, compCounit]; bicategory
    _ = 𝟙 _ ⊗≫ (leftZigzag adj₁.unit adj₁.counit) ▷ f₂ ⊗≫ f₁ ◁ (leftZigzag adj₂.unit adj₂.counit) ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = _ := by simp_rw [left_triangle]; bicategory
Похожие утверждения