English
For a finite index set α and a family σ, there is a canonical comparison map from the value of a condensed object on the finite coproduct to the product of the values on components.
Русский
Для конечного множества индексов α и семейства σ существует каноническое отображение сравнения от значения конденсированного объекта на конечной coproduct к произведению значений по компонентам.
LaTeX
$$$\\sigmaComparison : X.obj\\langle(\\mathrm{of}\\;P((a:\\alpha) \\times \\sigma a))\\rangle \\to \\Big( a:\\alpha \\mapsto X.obj\\langle\\mathrm{of}\\;P(\\sigma a)\\rangle \\Big)$$
Lean4
/-- The comparison map from the value of a condensed set on a finite coproduct to the product of the
values on the components.
-/
def sigmaComparison : X.obj ⟨(of P ((a : α) × σ a))⟩ ⟶ ((a : α) → X.obj ⟨of P (σ a)⟩) := fun x a ↦
X.map (ofHom _ ⟨Sigma.mk a, continuous_sigmaMk⟩).op x
