{-# OPTIONS --prop --rewriting #-}
module PropLogic where

open import Agda.Primitive public

----------------------------------------------------------------------
-- Heterogeneous propositional equality
----------------------------------------------------------------------
infix 4 _===_
data _===_
  {l : Level}
  {A : Set l}
  : --------------------------------
  {B : Set l}(x : A)(y : B) → Prop l
  where
  instance refl : {x : A} → x === x

{-# BUILTIN REWRITE _===_ #-}

symm :
  {l : Level}
  {A B : Set l}
  {x : A}
  {y : B}
  (p : x === y)
  → ---------
  y === x
symm refl = refl

infix  1 proof_
proof_ :
  {l : Level}
  {A B : Set l}
  {x : A}
  {y : B}
  → -------------
  x === y → x === y
proof p = p

infixr 2 _=[_]_
_=[_]_ :
  {l : Level}
  {A B C : Set l}
  (x : A)
  {y : B}
  {z : C}
  → ----------------------
  x === y → y === z → x === z
_ =[ refl ] q = q

infix  3 _qed
_qed :
  {l : Level}
  {A : Set l}
  (x : A)
  → ---------
  x === x
_ qed = refl

----------------------------------------------------------------------
-- Homogeneous propositional equality
----------------------------------------------------------------------
infix 4 _==_
_==_ : {l : Level}{A : Set l}(x y : A) → Prop l
_==_ = _===_

----------------------------------------------------------------------
-- Conjunction
----------------------------------------------------------------------
infixr 3 _∧_
data _∧_ {l m : Level}(P : Prop l)(Q : Prop m) : Prop (l ⊔ m) where
  ∧intro : P → Q → P ∧ Q

----------------------------------------------------------------------
-- Exists
----------------------------------------------------------------------
infix  1 ∃
data ∃ {l m : Level}(A : Set l)(P : A → Prop m) : Prop (l ⊔ m) where
  ∃intro : (x : A)(p : P x) → ∃ A P

syntax ∃ A (λ x → P) = ∃ x ∶ A , P

----------------------------------------------------------------------
-- Unique existence
----------------------------------------------------------------------
infix  1 ∃!
∃! : {l m : Level}(A : Set l)(P : A → Prop m) → Prop (l ⊔ m)
∃! A P = ∃ x ∶ A , (P x ∧ ∀(x' : A) → P x' → x == x')

syntax ∃! A (λ x → P) = ∃! x ∶ A , P

----------------------------------------------------------------------
-- Comprehension
----------------------------------------------------------------------
infix 0 _∣_
data subset {l m : Level}(A : Set l)(P : A → Prop m) : Set (l ⊔ m)
  where
  _∣_ : (x : A)(p : P x) → subset A P

syntax subset A (λ x → P) = subset x ∶ A , P

elt :
  {l m : Level}
  {A : Set l}
  {P : A → Prop m}
  → --------------
  subset A P → A
elt (x ∣ _) = x

prf :
  {l m : Level}
  {A : Set l}
  {P : A → Prop m}
  (z : subset A P)
  → --------------
  P (elt z)
prf (_ ∣ p) = p

subsetext :
  {l m : Level}
  {A : Set l}
  {P : A → Prop m}
  {z z' : subset A P}
  (_ : elt z == elt z')
  → -------------------
  z == z'
subsetext {z = _ ∣ _} {_ ∣ _} refl = refl

----------------------------------------------------------------------
-- The Axiom of Unique Choice
----------------------------------------------------------------------
postulate
  A!C : {l : Level}{A : Set l} → (∃ x ∶ A , ∀(x' : A) → x == x') → A

----------------------------------------------------------------------
-- Definite description
----------------------------------------------------------------------
module _
  {l m : Level}
  (A : Set l)
  (P : A → Prop m)
  where
  private
    AP : Set (l ⊔ m)
    AP = subset A P

    ∃!AP : ∃! A P → ∃ z ∶ AP , ∀(z' : AP) → z == z'
    ∃!AP (∃intro x (∧intro p q)) =
      ∃intro (x ∣ p) λ{(x' ∣ p') → subsetext (q x' p')}

  the : {{∃! A P}} → A
  the {{u}} = elt (A!C (∃!AP u))

  the-prf : {{_ : ∃! A P}} → P the
  the-prf {{u}} = prf (A!C (∃!AP u))

  the-uniq : {{_ : ∃! A P}}(x : A) → P x → the == x
  the-uniq {{∃intro x' (∧intro p' q)}} x p =
    let
      instance
        _ : ∃! A P
        _ = ∃intro x' (∧intro p' q)
    in
    proof
      the
    =[ symm (q the the-prf) ]
      x'
    =[ q x p ]
      x
    qed

  syntax the A (λ x → P) = the x ∶ A , P