C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ (↑Fin.castSucc i)) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ (Fin.succ j)) ≫ X.map (SimplexCategory.σ i)
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ X (↑Fin.castSucc i) ≫ σ X j = σ X (Fin.succ j) ≫ σ X i
dsimp [δ, σ]
no goals
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ (↑Fin.castSucc i)) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ (Fin.succ j)) ≫ X.map (SimplexCategory.σ i)
simp only [← X.map_comp, SimplexCategory.σ_comp_σ H]