{-# OPTIONS --guardedness #-}
{-
MGS 23 : Type Theory

Tuesday
-}

open import mon-lib

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 ∨ ¬ P) ⇒ ((¬ (P ∧ Q)) ⇔ ((¬ P) ∨ (¬ Q)))
proj₁ (dm2 (inj₁ x)) h = inj₂ (λ q → h (x , q))
proj₁ (dm2 (inj₂ x)) h = inj₁ x
proj₂ (dm2 _) (inj₁ np) (p , q) = np p
proj₂ (dm2 _) (inj₂ nq) (p , q) = nq q

-- P ∨ ¬ P principle of excluded middle
-- ¬ ¬ P → P indirect proof

-- inductive types

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ -- successor

one = suc zero
two = suc one

{-# BUILTIN NATURAL ℕ #-}

seventeen : ℕ
seventeen = 17

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

_*_ : ℕ → ℕ → ℕ
zero * n = zero
suc m * n = n + (m * n)

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A → Maybe A

pred : ℕ → Maybe ℕ
pred zero = nothing
pred (suc x) = just x

zerosuc : Maybe ℕ → ℕ
zerosuc nothing = zero
zerosuc (just x) = suc x

-- coinductive type
-- conatural numbers

record ℕ∞ : Set where
  coinductive
  field
    pred∞ : Maybe ℕ∞

open ℕ∞

zero∞ : ℕ∞
pred∞ zero∞ = nothing

suc∞ : ℕ∞ → ℕ∞
pred∞ (suc∞ x) = just x

∞ : ℕ∞
pred∞ ∞ = just ∞

{-
_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)
-}

_+∞_ : ℕ∞ → ℕ∞ → ℕ∞
pred∞ (m +∞ n) with pred∞ m
... | nothing = pred∞ n
... | just m' = just (m' +∞ n)