Sigma types #
This file proves basic results about sigma types.
A sigma type is a dependent pair type. Like α × β
but where the type of the second component
depends on the first component. More precisely, given β : ι → Type*
, Sigma β
is made of stuff
which is of type β i
for some i : ι
, so the sigma type is a disjoint union of types.
For example, the sum type X ⊕ Y
can be emulated using a sigma type, by taking ι
with
exactly two elements (see Equiv.sumEquivSigmaBool
).
Σ x, A x
is notation for Sigma A
(note that this is \Sigma
, not the sum operator ∑
).
Σ x y z ..., A x y z ...
is notation for Σ x, Σ y, Σ z, ..., A x y z ...
. Here we have
α : Type*
, β : α → Type*
, γ : Π a : α, β a → Type*
, ...,
A : Π (a : α) (b : β a) (c : γ a b) ..., Type*
with x : α
y : β x
, z : γ x y
, ...
Notes #
The definition of Sigma
takes values in Type*
. This effectively forbids Prop
- valued sigma
types. To that effect, we have PSigma
, which takes value in Sort*
and carries a more
complicated universe signature as a consequence.
Equations
- One or more equations did not get rendered due to their size.
A version of Iff.mp Sigma.ext_iff
for functions from a nonempty type to a sigma type.
Equations
- One or more equations did not get rendered due to their size.
Map the left and right components of a sigma