```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  5 ∥_∥
∥_∥ : {ℓ : Level} → Set ℓ → Set ℓ
∥ A ∥ = A / ∇

infix  5 _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 3 _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  1 ∃
∃ :
{ℓ ℓ' : Level}
(A : Set ℓ)
(B : A → Set ℓ')
→ --------------
Set(ℓ ⊔ ℓ')
∃ A B = ∥ Σ A B ∥

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

----------------------------------------------------------------------
-- Comprehension
----------------------------------------------------------------------
infix 3 _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)

```