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