pprod α β is equivalent to α × β

Product of two equivalences, in terms of pprod. If α ≃ β and γ ≃ δ, then pprod α γ ≃ pprod β δ.

Combine two equivalences using pprod in the domain and prod in the codomain.

Combine two equivalences using pprod in the codomain and prod in the domain.

pprod α β is equivalent to plift α × plift β

Product of two equivalences. If α₁ ≃ α₂ and β₁ ≃ β₂, then α₁ × β₁ ≃ α₂ × β₂. This is prod.map as an equivalence.

Type product is commutative up to an equivalence: α × β ≃ β × α. This is prod.swap as an equivalence.

Type product is associative up to an equivalence.

Four-way commutativity of prod. The name matches mul_mul_mul_comm.

Functions on α × β are equivalent to functions α → β → γ.

punit is a right identity for type product up to an equivalence.

punit is a left identity for type product up to an equivalence.

Any unique type is a right identity for type product up to equivalence.

Any unique type is a left identity for type product up to equivalence.

empty type is a right absorbing element for type product up to an equivalence.

empty type is a left absorbing element for type product up to an equivalence.

pempty type is a right absorbing element for type product up to an equivalence.

pempty type is a left absorbing element for type product up to an equivalence.

psum is equivalent to sum.

If α ≃ α' and β ≃ β', then α ⊕ β ≃ α' ⊕ β'. This is sum.map as an equivalence.

If α ≃ α' and β ≃ β', then psum α β ≃ psum α' β'.

Combine two equivs using psum in the domain and sum in the codomain.

Combine two equivs using sum in the domain and psum in the codomain.

Combine a permutation of α and of β into a permutation of α ⊕ β.

bool is equivalent the sum of two punits.

Sum of types is commutative up to an equivalence. This is sum.swap as an equivalence.

Sum of types is associative up to an equivalence.

Sum with empty is equivalent to the original type.

The sum of empty with any Sort* is equivalent to the right summand.

option α is equivalent to α ⊕ punit

The set of x : option α such that is_some x is equivalent to α.

The product over option α of β a is the binary product of the product over α of β (some α) and β none

α ⊕ β is equivalent to a sigma-type over bool. Note that this definition assumes α and β to be types from the same universe, so it cannot by 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.

sigma_fiber_equiv f for f : α → β is the natural equivalence between the type of all fibres of f and the total space α.

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 subtype_or_equiv for sum types over subtypes {x // p x} and {x // q x} that are not necessarily is_compl p q.

Combines an equiv between two subtypes with an equiv between their complements to form a permutation.

Combining permutations on ε that permute only inside or outside the subtype split induced by p : ε → Prop constructs a permutation on ε.

For a fixed function x₀ : {a // p a} → β defined on a subtype of α, the subtype of functions x : α → β that agree with x₀ on the subtype {a // p a} is naturally equivalent to the type of functions {a // ¬ p a} → β.

A family of equivalences Π a, β₁ a ≃ β₂ a generates an equivalence between Π a, β₁ a and Π a, β₂ a.

Given φ : α → β → Sort*, we have an equivalence between Π a b, φ a b and Π b a, φ a b. This is function.swap as an equiv.

Dependent curry equivalence: the type of dependent functions on Σ i, β i is equivalent to the type of dependent functions of two arguments (i.e., functions to the space of functions).

This is sigma.curry and sigma.uncurry together as an equiv.

A family of equivalences Π (a : α₁), β₁ ≃ β₂ generates an equivalence between β₁ × α₁ and β₂ × α₁.

A family of equivalences Π (a : α₁), β₁ ≃ β₂ generates an equivalence between α₁ × β₁ and α₁ × β₂.

A family of equivalences between fibers gives an equivalence between domains.

A variation on equiv.prod_congr where the equivalence in the second component can depend on the first component. A typical example is a shear mapping, explaining the name of this declaration.

prod_extend_right a e extends e : perm β to perm (α × β) by sending (a, b) to (a, e b) and keeping the other (a', b) fixed.

The type of functions to a product α × β is equivalent to the type of pairs of functions γ → α and γ → β.

The type of functions on a sum type α ⊕ β is equivalent to the type of pairs of functions on α and on β.

Type product is right distributive with respect to type sum up to an equivalence.

Type product is left distributive with respect to type sum up to an equivalence.