∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.SmallCategory C] {X' : SSet.Truncated 2} (ψ : X ⟶ X')
  (φ : X' ⟶ (SSet.truncation 2).obj (CategoryTheory.nerve C)),
  SSet.Truncated.HomotopyCategory.descOfTruncation (CategoryTheory.CategoryStruct.comp ψ φ) =
    (SSet.Truncated.mapHomotopyCategory ψ).comp (SSet.Truncated.HomotopyCategory.descOfTruncation φ)