Equivalence between sum types #
In this file we continue the work on equivalences begun in Mathlib/Logic/Equiv/Defs.lean
, defining
canonical isomorphisms between various types: e.g.,
Equiv.sumEquivSigmaBool
is the canonical equivalence between the sum of two typesα ⊕ β
and the sigma-typeΣ b, bif b then β else α
;Equiv.prodSumDistrib : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ)
shows that type product and type sum satisfy the distributive law up to a canonical equivalence;
More definitions of this kind can be found in other files.
E.g., Mathlib/Algebra/Equiv/TransferInstance.lean
does it for many algebraic type classes like
Group
, Module
, etc.
Tags #
equivalence, congruence, bijective map
α ⊕ β
is equivalent to a Sigma
-type over Bool
. Note that this definition assumes α
and
β
to be types from the same universe, so it cannot be used directly to transfer theorems about
sigma types to theorems about sum types. In many cases one can use ULift
to work around this
difficulty.
Equations
Instances For
Inhabited types are equivalent to Option β
for some β
by identifying default
with none
.
Equations
Instances For
For any predicate p
on α
,
the sum of the two subtypes {a // p a}
and its complement {a // ¬ p a}
is naturally equivalent to α
.
See subtypeOrEquiv
for sum types over subtypes {x // p x}
and {x // q x}
that are not necessarily IsCompl p q
.
Equations
Instances For
An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums. Compare
with Equiv.sumSigmaDistrib
which is indexed by sums.
Equations
Instances For
A type indexed by disjoint sums of types is equivalent to the sum of the sums. Compare with
Equiv.sigmaSumDistrib
which has the sums as the output type.