C : Type u
inst✝ : Category C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [0]
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ f ≫ X.map (SimplexCategory.const [0] 0) = f
C : Type u
inst✝ : Category C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [0]
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ (augment X X₀ f w).hom.app [0] = f
dsimp
no goals
C : Type u
inst✝ : Category C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [0]
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ f ≫ X.map (SimplexCategory.const [0] 0) = f
rw [SimplexCategory.hom_zero_zero ([0].const 0), X.map_id, Category.comp_id]