mk_naturality_σ00 — Mathlib

English

A variant of congr_mk₁_map for ReflQuiver with explicit hx hy identifications ensures mk₁ equality.

Русский

Вариант congr_mk₁_map для ReflQuiver с явной идентификацией hx hy обеспечивает равенство mk₁.

LaTeX

$$$\text{same as above in a less syntactic form}$$$

Lean4

theorem mk_naturality_σ00 : toNerve₂.mk.naturalityProperty F (σ₂ (n := 0) 0) :=
  by
  ext x
  refine Eq.trans ?_ (nerve.σ₀_mk₀_eq (C := C) (F.obj x)).symm
  have := ReflPrefunctor.map_id F x
  dsimp at this ⊢
  rw [← this, ← OneTruncation₂.id_edge x]
  fapply ReflPrefunctor.congr_mk₁_map
  · simp [← FunctorToTypes.map_comp_apply, ← op_comp]
  · simp [← FunctorToTypes.map_comp_apply, ← op_comp]
  · aesop

Похожие утверждения