{-# OPTIONS --guardedness #-}
{- small library for MGS 2023 -}

{- products and sums -}

infix 10 _×_
record _×_ (A B : Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

open _×_ public

variable
  A B C M : Set

curry : (A × B → C) → (A → B → C)
curry f a b = f (a , b) -- C-c C-,
uncurry : (A → B → C) → (A × B → C)
uncurry f (a , b) = f a b

infix 5 _⊎_
data _⊎_(A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

case : (A → C) → (B → C) → (A ⊎ B → C)
case f g (inj₁ a) = f a
case f g (inj₂ b) = g b

uncase : (A ⊎ B → C) → (A → C) × (B → C)
uncase f = (λ a → f (inj₁ a)) , λ b → f (inj₂ b)

case' : (A → C) × (B → C) → (A ⊎ B → C)
case' = uncurry case

record ⊤ : Set where
  constructor tt

open ⊤ public

data ⊥ : Set where

case⊥ : ⊥ → A
case⊥ ()


{- prop logic -}

prop = Set

variable
  P Q R : prop

infix 3 _∧_
_∧_ : prop → prop → prop
P ∧ Q = P × Q

infix 2 _∨_
_∨_ : prop → prop → prop
P ∨ Q = P ⊎ Q

infixr 1 _⇒_
_⇒_ : prop → prop → prop
P ⇒ Q = P → Q

False : prop
False = ⊥

True : prop
True = ⊤

¬_ : prop → prop
¬ P = P ⇒ False

infix 0 _⇔_
_⇔_ : prop → prop → prop
P ⇔ Q = (P ⇒ Q) ∧ (Q ⇒ P)

efq : False ⇒ P
efq = case⊥