Lean4
/-- If `ed` is an extra degeneracy for `X : SimplicialObject.Augmented C` and
`F : C ⥤ D` is a functor, then `ed.map F` is an extra degeneracy for the
augmented simplicial object in `D` obtained by applying `F` to `X`. -/
def map {D : Type*} [Category D] {X : SimplicialObject.Augmented C} (ed : ExtraDegeneracy X) (F : C ⥤ D) :
ExtraDegeneracy (((whiskering _ _).obj F).obj X)
where
s' := F.map ed.s'
s n := F.map (ed.s n)
s'_comp_ε := by
dsimp
rw [comp_id, ← F.map_comp, ed.s'_comp_ε]
dsimp only [point_obj]
rw [F.map_id]
s₀_comp_δ₁ := by
dsimp
rw [comp_id, ← F.map_comp]
dsimp [SimplicialObject.whiskering, SimplicialObject.δ]
rw [← F.map_comp]
erw [ed.s₀_comp_δ₁]
s_comp_δ₀
n := by
dsimp [SimplicialObject.δ]
rw [← F.map_comp]
erw [ed.s_comp_δ₀]
dsimp
rw [F.map_id]
s_comp_δ n
i := by
dsimp [SimplicialObject.δ]
rw [← F.map_comp, ← F.map_comp]
erw [ed.s_comp_δ]
rfl
s_comp_σ n
i := by
dsimp [SimplicialObject.whiskering, SimplicialObject.σ]
rw [← F.map_comp, ← F.map_comp]
erw [ed.s_comp_σ]
rfl
