English
The representation function repr for Sigma F sends a Sigma F-object to its polynomial representation by composing the representations of its components.
Русский
Функция представления Sigma F переводит объект Sigma F в его полиномиальное представление, комбинируя представления компонент.
LaTeX
$$$\\\\mathrm{repr} : ΣF α \\to (ΣP F α), \\\\mathrm{repr}(⟨a,x⟩) = ⟨⟨a, x⟩, \\\\text{rest}\\\\rangle.$$$
Lean4
instance : MvQPF (Sigma F) where
P := Sigma.P F
abs {α} := @Sigma.abs _ _ F _ α
repr {α} := @Sigma.repr _ _ F _ α
abs_repr := by rintro α ⟨x, f⟩; simp only [Sigma.abs, Sigma.repr, Sigma.eta, abs_repr]
abs_map := by
rintro α β f ⟨x, g⟩; simp only [Sigma.abs, MvPFunctor.map_eq]
simp only [(· <$$> ·), ← abs_map, ← MvPFunctor.map_eq]
