def SSet.Truncated.truncEquiv {S : SSet} (m : ℕ) {a : SimplexCategory} (ha : a.len ≤ m := by trunc) : S.obj (Opposite.op a) ≃ ((truncation m).obj S).obj (Opposite.op { obj := a, property := ha })

The idea behind this trivial equivalence and trunc_map, trunc_map' is to make explicit whether an object is in a truncated simplicial set; this allows us to replace dsimps in proofs by rws.

Equations

• SSet.Truncated.truncEquiv m ha = { toFun := id, invFun := id, left_inv := ⋯, right_inv := ⋯ }

theorem SSet.Truncated.trunc_map {S : SSet} {m : ℕ} {a b : SimplexCategory} (ha : a.len ≤ m := by trunc) (hb : b.len ≤ m := by trunc) {f : a ⟶ b} {σ : S.obj (Opposite.op b)} : ((truncation m).obj S).map (SimplexCategory.Truncated.Hom.tr f ha hb).op ((truncEquiv m hb) σ) = S.map f.op σ

theorem SSet.Truncated.trunc_map' {S : SSet} {m : ℕ} {a b : SimplexCategory} (ha : a.len ≤ m := by trunc) (hb : b.len ≤ m := by trunc) {f : a ⟶ b} {σ : ((truncation m).obj S).obj (Opposite.op { obj := b, property := hb })} : ((truncation m).obj S).map (SimplexCategory.Truncated.Hom.tr f ha hb).op σ = S.map f.op σ