C : Type u
inst✝ : Category C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ (Fin.succ i)).op = 𝟙 (X.obj [n].op)
C : Type u
inst✝ : Category C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ σ X i ≫ δ X (Fin.succ i) = 𝟙 (X.obj [n].op)
dsimp [δ, σ]
no goals
C : Type u
inst✝ : Category C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ (Fin.succ i)).op = 𝟙 (X.obj [n].op)
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_succ, op_id, X.map_id]