Theorems · Theorem · category theory

TopCat.Homotopy.h_comp

∀ {X Y Z : TopCat} {f₀ f₁ : X ⟶ Y} {g₀ g₁ : Y ⟶ Z} (G : TopCat.Homotopy g₀ g₁) (F : TopCat.Homotopy f₀ f₁),
  (G.comp F).h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X
        (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id TopCat.I)
          (CategoryTheory.CategoryStruct.id TopCat.I)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X TopCat.I TopCat.I).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight F.h TopCat.I) G.h))

Defined in

Mathlib.Topology.Homotopy.TopCat.Basic

Cited by

0 results in Mathlib

Foundations

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