English
Destructor for Cofix F: Cofix.dest extracts the one-step structure from a Cofix value, yielding an F-structure over an extended index.
Русский
Деструктор Cofix F: Cofix.dest извлекает структуру одного шага из значения Cofix, получая структуру типа F над расширенным индексом.
LaTeX
$$$\\mathrm{dest} : \\mathrm{Cofix}\\,F\\,\\alpha \\to F(\\alpha\\append1(\\mathrm{Cofix}\\,F\\,\\alpha)).$$$
Lean4
/-- Destructor for `Cofix F` -/
def dest {α : TypeVec n} : Cofix F α → F (α.append1 (Cofix F α)) :=
Quot.lift (fun x => appendFun id (Quot.mk Mcongr) <$$> abs (M.dest q.P x))
(by
rintro x y ⟨r, pr, rxy⟩
dsimp
have : ∀ x y, r x y → Mcongr x y := by
intro x y h
exact ⟨r, pr, h⟩
rw [← Quot.factor_mk_eq _ _ this]
conv =>
lhs
rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map, ← appendFun_comp_id])
