{-# OPTIONS --without-K  #-}
module sum where

open import level using (Level; _⊔_)

infixr  _,_
infixr  _×_
infixr  _⊎_

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

_×_ : {l k : Level} (A : Set l) (B : Set k) → Set (l ⊔ k)
A × B = Σ A λ _ → B

uncurry : ∀ {i j k}{X : Set i}{Y : Set j}{Z : Set k}
        → (X → Y → Z)
        → (X × Y) → Z
uncurry f (x , y) = f x y

data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B