English
Any Unique type over α yields a right identity for the dependent sigma-type: (i, b) ∈ Σ i, β(i) ≃ β(default).
Русский
Любой уникальный тип над α задает правое тождество для зависимого сигма-типа: (i, b) ∈ Σ i, β(i) ≃ β(default).
LaTeX
$$$$ (i:\\alpha) \\times \\beta(i) \\simeq \\beta(\\mathrm{default}). $$$$
Lean4
/-- Any `Unique` type is a left identity for type sigma up to equivalence. Compare with `uniqueProd`
which is non-dependent. -/
def uniqueSigma {α} (β : α → Type*) [Unique α] : (i : α) × β i ≃ β default
where
toFun := fun p ↦ (Unique.eq_default _).rec p.2
invFun := fun b ↦ ⟨default, b⟩
left_inv := fun _ ↦ Sigma.ext (Unique.default_eq _) (eqRec_heq _ _)
