English
A product-valued analogue of a Segal map: the 2-simplex nerve object maps into a product of two 1-simplex nerve objects via projections ev01₂ and ev12₂, forming a Segal-like comparison.
Русский
Аналог Segal-карты, где 2-симплекс нервного объекта отображается в произведение двух 1-симплекс нервных объектов через проекции ev01₂ и ev12₂, образуя сравнение типа Segal.
LaTeX
$$$\mathrm{nerve₂.seagull}(C) : (\mathrm{nerve₂.obj}\;C)_{op} \to (\mathrm{nerve₂.obj}\;C)_{1} \times (\mathrm{nerve₂.obj}\;C)_{1}$ via $\mathrm{ev}_{01}$ and $\mathrm{ev}_{12}$$$
Lean4
/-- A computation about `toNerve₂.mk'`. -/
theorem oneTruncation₂_toNerve₂Mk' : oneTruncation₂.map (toNerve₂.mk' F hyp) = F :=
by
refine
ReflPrefunctor.ext (fun _ ↦ ComposableArrows.ext₀ rfl)
(fun X Y g ↦ eq_of_heq (heq_eqRec_iff_heq.2 <| heq_eqRec_iff_heq.2 ?_))
simp [oneTruncation₂]
refine Quiver.heq_of_homOfEq_ext ?_ ?_ (f' := F.map g) ?_
· exact ComposableArrows.ext₀ rfl
· exact ComposableArrows.ext₀ rfl
· apply OneTruncation₂.Hom.ext
simp only [oneTruncation₂_obj, ReflQuiv.of_val, OneTruncation₂.homOfEq_edge]
fapply ComposableArrows.ext₁ <;> simp [ReflQuiv.comp_eq_comp]
· rw [g.src_eq]; exact congr_arg (·.obj 0) (F.map g).src_eq.symm
· rw [g.tgt_eq]; exact congr_arg (·.obj 1) (F.map g).tgt_eq.symm
· refine (conj_eqToHom_iff_heq' _ _ _ _).2 ?_
simp [OneTruncation₂.nerveHomEquiv]
obtain ⟨g, rfl, rfl⟩ := g
rfl
