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

open import level using (Level; _⊔_)
open import function.core

infixr 4 _,_
infixr 2 _×_
infixr 1 _⊎_

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 :  {a b c} {A : Set a} {B : A  Set b} {C : (x : A)  (B x)  Set c}
         ((x : A)  (y : B x)  C x y)  ((xy : Σ A B)  C (proj₁ xy) (proj₂ xy))
uncurry f (a , b) = f 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

[_,⊎_] :  {i i' j}{A : Set i}{A' : Set i'}{B : Set j}
       (A  B)  (A'  B)
       A  A'  B
[ f ,⊎ f' ] (inj₁ a) = f a
[ f ,⊎ f' ] (inj₂ a') = f' a'

map-⊎ :  {i i' j j'}{A : Set i}{A' : Set i'}
       {B : Set j}{B' : Set j'}
       (A  B)  (A'  B')
       A  A'  B  B'
map-⊎ g g' = [ inj₁ ∘' g ,⊎ inj₂ ∘' g' ]