{-
MGS 23 : Type Theory

Monday
-}

variable A B C : Set

record _×_ (A B : Set) : Set where
  field
    proj₁ : A
    proj₂ : B

open _×_

_,_ : A → B → A × B
proj₁ (a , b) = a
proj₂ (a , b) = b

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

uncurry : (A → B → C) → (A × B → C)
uncurry f ab = f (proj₁ ab ) (proj₂ ab)

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

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

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

record ⊤ : Set where

tt : ⊤
tt = record {}

data ⊥ : Set where

case⊥ : ⊥ → C
case⊥ ()

-- logic

prop = Set

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

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

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

False : prop
False = ⊥

¬ : prop → prop
¬ P = P ⇒ False

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

variable P Q R : prop

dm1 : (¬ (P ∨ Q)) ⇔ ((¬ P) ∧ (¬ Q))
proj₁ dm1 h = (λ p → h (inj₁ p)) , λ q → h (inj₂ q)
proj₂ dm1 npnq (inj₁ p) = proj₁ npnq p
proj₂ dm1 npnq (inj₂ q) = proj₂ npnq q

dm2 : (¬ (P ∧ Q)) ⇔ ((¬ P) ∨ (¬ Q))
dm2 = {!!}