| 123456789101112131415 |
- module Common.Sum where
- open import Common.Level
- data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
- inj₁ : (x : A) → A ⊎ B
- inj₂ : (y : B) → A ⊎ B
- [_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : A ⊎ B → Set c} →
- ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
- ((x : A ⊎ B) → C x)
- [ f , g ] (inj₁ x) = f x
- [ f , g ] (inj₂ y) = g y
|
