Theorems · Theorem · category theory

SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk

∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.SmallCategory C]
  (φ : X ⟶ (SSet.truncation 2).obj (CategoryTheory.nerve C))
  {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })} (e : SSet.Truncated.Edge x₀ x₁),
  (SSet.Truncated.HomotopyCategory.descOfTruncation φ).map (SSet.Truncated.HomotopyCategory.homMk e) =
    CategoryTheory.nerve.homEquiv (e.map φ)

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategory