module Proposition where

open import Empty
open import Equality
open import Function
open import Level
open import Product
open import Quotient
open import Sum
open import UIP

----------------------------------------------------------------------
-- Negation
----------------------------------------------------------------------
¬ : {ℓ : Level} → Set ℓ → Set ℓ
¬ {ℓ} A = A → Ø {ℓ}

----------------------------------------------------------------------
-- Indiscrete relation
----------------------------------------------------------------------
data ∇ {ℓ : Level}{A : Set ℓ} : A → A → Set ℓ where
  ∇rel : {x y : A} →  ∇ x y

----------------------------------------------------------------------
-- Propositional truncation via quotients
----------------------------------------------------------------------
infix   ∥_∥
∥_∥ : {ℓ : Level} → Set ℓ → Set ℓ
∥ A ∥ = A / ∇ 

infix   _mod∇
_mod∇ :{ℓ : Level}{A : Set ℓ} → A → ∥ A ∥
x mod∇ = [ x ]/ ∇

∥∥elim :
  {ℓ ℓ' : Level}
  {A : Set ℓ}
  (B : ∥ A ∥ → Set ℓ')
  (f : (x : A)  → B (x mod∇))
  (_ : (x x' : A) → subst B (by ∇rel) (f x) ≡ f x')
  → -----------------------------------------------
  (y : ∥ A ∥) → B y
∥∥elim B f e = qelim ∇ B f (λ x x' _ → e x x')

∥∥comp :
  {ℓ ℓ' : Level}
  {A : Set ℓ}
  (B : ∥ A ∥ → Set ℓ')
  (f : (x : A)  → B (x mod∇))
  (e : (x x' : A) → subst B (by ∇rel) (f x) ≡ f x')
  (x : A)
  → -----------------------------------------------
  ∥∥elim B f e (x mod∇) ≡ f x
∥∥comp B f e x  = qcomp ∇ B f (λ x x' _ → e x x') x

∥∥rec :
  {ℓ ℓ' : Level}
  {A : Set ℓ}
  {B : Set ℓ'}
  (f : A → B)
  (_ : (x x' : A) → f x ≡ f x')
  → ---------------------------
  ∥ A ∥ → B
∥∥rec f e = qrec ∇ _ f (λ x x' _ → e x x')

∥∥rec-comp :
  {ℓ ℓ' : Level}
  {A : Set ℓ}
  {B : Set ℓ'}
  (f : A → B)
  (e : (x x' : A) → f x ≡ f x')
  (x : A)
  → ---------------------------
  ∥∥rec f e (x mod∇) ≡ f x
∥∥rec-comp f e x = qrec-comp ∇ _ f (λ x x' _ → e x x') x

----------------------------------------------------------------------
-- Mere propositions
----------------------------------------------------------------------
isProp :
  {ℓ : Level}
  (A : Set ℓ)
  → ---------
  Set ℓ
isProp A = {x y : A} → x ≡ y

∥∥isProp :
  {ℓ : Level}
  {A : Set ℓ}
  → ------------
  isProp (∥ A ∥)
∥∥isProp {y = q} =
  qelim ∇ (λ p' → p' ≡ q) (f q) (λ _ _ _ → uip) _
  where
  f : (q' : ∥ _ ∥)(x : _) → (x mod∇) ≡ q'
  f q' x =
    qelim ∇ (λ q' → (x mod∇) ≡ q') (λ y → by ∇rel) (λ _ _ _ → uip) q'
    
----------------------------------------------------------------------
-- Mere disjunction
----------------------------------------------------------------------
infixr  _or_
_or_ : {ℓ : Level} → Set ℓ → Set ℓ → Set ℓ
A or B = ∥ A ⊎ B ∥

orcompat :
  {ℓ ℓ' : Level}
  {A B : Set ℓ}
  {C : Set ℓ'}
  {f : A → C}
  {g : B → C}
  (u : (x x' : A) → f x ≡ f x')
  (v : (y y' : B) → g y ≡ g y')
  (w : (x : A)(y : B) → f x ≡ g y)
  (z z' : A ⊎ B)
  → ------------------------------
  [ f ∣ g ] z ≡ [ f ∣ g ] z'
orcompat u _ _ (inl x) (inl x') = u x x'
orcompat _ _ w (inl x) (inr y)  = w x y
orcompat _ _ w (inr y) (inl x)  = symm (w x y)
orcompat _ v _ (inr y) (inr y') = v y y'

orrec :
  {ℓ ℓ' : Level}
  {A B : Set ℓ}
  {C : Set ℓ'}
  (f : A → C)
  (g : B → C)
  (u : (x x' : A) → f x ≡ f x')
  (v : (y y' : B) → g y ≡ g y')
  (w : (x : A)(y : B) → f x ≡ g y)
  → ------------------------------
  A or B → C
orrec f g u v w = ∥∥rec [ f ∣ g ] (orcompat u v w)

orcompl :
  {ℓ ℓ' : Level}
  {A B : Set ℓ}
  {C : Set ℓ'}
  (f : A → C)
  (g : B → C)
  (u : (x x' : A) → f x ≡ f x')
  (v : (y y' : B) → g y ≡ g y')
  (w : (x : A)(y : B) → f x ≡ g y)
  (x : A)
  → ---------------------------------
  orrec f g u v w (inl x mod∇) ≡ f x
orcompl f g u v w  = (∥∥rec-comp [ f ∣ g ] (orcompat u v w)) ∘ inl

orcompr :
  {ℓ ℓ' : Level}
  {A B : Set ℓ}
  {C : Set ℓ'}
  (f : A → C)
  (g : B → C)
  (u : (x x' : A) → f x ≡ f x')
  (v : (y y' : B) → g y ≡ g y')
  (w : (x : A)(y : B) → f x ≡ g y)
  (y : B)
  → --------------------------------
  orrec f g u v w (inr y mod∇) ≡ g y
orcompr f g u v w  = (∥∥rec-comp [ f ∣ g ] (orcompat u v w)) ∘ inr
 
----------------------------------------------------------------------
-- Mere existence
----------------------------------------------------------------------
infix   ∃
∃ :
  {ℓ ℓ' : Level}
  (A : Set ℓ)
  (B : A → Set ℓ')
  → --------------
  Set(ℓ ⊔ ℓ')
∃ A B = ∥ Σ A B ∥

syntax ∃ A (λ x → B) = ∃ x ∈ A , B

----------------------------------------------------------------------
-- Comprehension
----------------------------------------------------------------------
infix  _by_
record subset
  {ℓ ℓ' : Level}
  (A : Set ℓ)
  (P : A → Set ℓ') : Set (ℓ ⊔ ℓ') where
  constructor _by_
  field
    inc     : A
    prfinc  : ∥ P inc ∥

open subset public

syntax subset A (λ x → P) = ⟦ x ∈ A ∣ P ⟧

incInj :
  {ℓ ℓ' : Level}
  {A : Set ℓ}
  {P : A → Set ℓ'}
  {a b : subset A P}
  → -------------------
  inc a ≡ inc b → a ≡ b
incInj {a = x by _} refl = cong (x by_) (∥∥isProp)