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