Coproduct types
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Elisabeth Bonnevier.
Created on 2023-01-20.
Last modified on 2023-09-10.
module foundation-core.coproduct-types where
Imports
open import foundation.universe-levels
Idea
The coproduct of two types A
and B
can be thought of as the disjoint union
of A
and B
.
Definition
infixr 10 _+_ data _+_ {l1 l2 : Level} (A : UU l1) (B : UU l2) : UU (l1 ⊔ l2) where inl : A → A + B inr : B → A + B ind-coprod : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (C : A + B → UU l3) → ((x : A) → C (inl x)) → ((y : B) → C (inr y)) → (t : A + B) → C t ind-coprod C f g (inl x) = f x ind-coprod C f g (inr x) = g x
Recent changes
- 2023-09-10. Fredrik Bakke. Define precedence levels and associativities for all binary operators (#712).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).
- 2023-04-28. Fredrik Bakke. Miscellaneous refactoring and small additions (#579).