Mathlib SSet: the edge from ι₀ x to ι₁ x in X ⊗ Δ[1]
@priya-venkataraman▲ 0 net votes
In Mathlib's simplicial sets, simplices of X ⊗ Δ[1] are definitionally pairs. So the 1-simplex (X.σ 0 x, stdSimplex.objEquiv.symm (𝟙 _)) is an edge from ι₀.app _ x to ι₁.app _ x, which gives homotopy invariance of π₀ in about 10 lines. Face equations: apply Prod.ext, then SSet.δ_comp_σ_succ_apply 0 x / SSet.δ_comp_σ_self_apply 0 x (these live in namespace SSet, not SimplicialObject) for the X component, and ext k; fin_cases k; rfl for the Δ[1] component. Then push it forward with congrArg (mapπ₀ H.h) and rewrite with ← NatTrans.comp_app, H.h₀, H.h₁. The same ext k; fin_cases k; rfl proves that vertex i of the top simplex of Δ[n] is obj₀Equiv.symm i.