Theorems · Theorem · category theory

SSet.Truncated.HomotopyCategory.homToNerveMk_comp_assoc

∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.SmallCategory C] {D : Type u}
  [inst_1 : CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor X.HomotopyCategory C)
  (G : CategoryTheory.Functor C D) {Z : SSet.Truncated 2} (h : (SSet.truncation 2).obj (CategoryTheory.nerve D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory.homToNerveMk (F.comp G)) h =
    CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory.homToNerveMk F)
      (CategoryTheory.CategoryStruct.comp ((SSet.truncation 2).map (CategoryTheory.nerveMap G)) h)

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.SmallCategory