Theorems · Definition · logic and foundations

Equiv.uniqueSigma

{α : Type u_10} → (β : α → Type u_9) → [inst : Unique α] → (i : α) × β i ≃ β default

Any Unique type is a left identity for type sigma up to equivalence. Compare with uniqueProd which is non-dependent.

Defined in

Mathlib.Logic.Equiv.Prod

Cited by

7 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

Unique