English
Dest is compatible with functorial map: mapping an α-structure to β-structure through g and dropping the corresponding components preserves the destination structure via a conjugate map.
Русский
Деструктор совместим с отображением структуры через g: перевод структуры α в β сохраняет разрушение через соответствующий отображатель.
LaTeX
$$$\forall {\alpha \beta : TypeVec n} (g : \alpha \Rightarrow \beta) (x : P.M \alpha), \\ M.dest P (g <$$> x) = (appendFun g (\lambda x. g <$$> x)) <$$> M.dest P x$$$
Lean4
theorem dest_map {α β : TypeVec n} (g : α ⟹ β) (x : P.M α) :
M.dest P (g <$$> x) = (appendFun g fun x => g <$$> x) <$$> M.dest P x :=
by
obtain ⟨a, f⟩ := x
rw [map_eq]
conv =>
rhs
rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]
rfl
