```-- Martin Escardo, 3rd August 2015, updated 6th August 2015
-- Modified 9th May to allow quantification over types of any universe.

{-
We develop some logic in the type Prp of propositions, where we
define the logical connectives and their introduction and
elimination rules following the ideas of the HoTT book. We then
prove that

false ≡ ∀ r. r
p ∧ q ≡ ∀ r. (p ⇒ q ⇒ r) ⇒ r
p ∨ q ≡ ∀ r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
∃ p   ≡ ∀ r. (∀ x. p(x) ⇒ r) ⇒ r
-}

{-# OPTIONS --without-K #-}
{-# OPTIONS --rewriting #-} -- Need because we import prop which now uses rewriting.

module logic where

open import preliminaries
open import prop
open import proptrunc
open import propisset

-- The two canonical truth values:

true : Prop
true = ₍ 𝟙 , 𝟙-isProp ₎

false : Prop
false = ₍ 𝟘 , 𝟘-isProp ₎

-- Propositional univalence gives that p holds ≡ (p ≡ true):

holds→equal-true : {p : Prop} → p holds → p ≡ true
holds→equal-true {p} h = Prop-≡ (propua (holdsIsProp p) (holdsIsProp true) (λ _ → zero) (λ _ → h))

equal-true→holds : {p : Prop} → p ≡ true → p holds
equal-true→holds {p} e = transport (λ X → X) (sym a) zero
where
a : p holds ≡ 𝟙
a = ap _holds e

holds-is-equal-true : (p : Prop) → p holds ≡ (p ≡ true)
holds-is-equal-true p = propua (holdsIsProp p) Prop-isSet holds→equal-true equal-true→holds

-- The logical connectives:

infixr 30 _⇒_
infixr 31 _∨_
infixr 32 _∧_

_∧_ _∨_ _⇒_ : Prop → Prop → Prop

p ∧ q = ₍ (p holds × q holds) , isProp-closed-under-Σ (holdsIsProp p) (λ _ → holdsIsProp q) ₎

p ⇒ q = ₍ (p holds → q holds) , isProp-exponential-ideal (λ _ → holdsIsProp q) ₎

p ∨ q = ₍ ∥ p holds + q holds ∥ , ∥∥-isProp ₎

-- The quantifiers.
--
-- Because "∀" is taken, and "∃" has a slightly different meaning in
-- the HoTT book, we will have to use something else. We write a
-- small, almost invisible, dot on top of them:

∀̇ : {i : Level} {X : Set i} → (X → Prop) → Prop
∀̇ p = ₍ resize₁ (∀ x → p x holds) isp , resize₁-isProp isp ₎
where
isp : isProp (∀ x → p x holds)
isp = isProp-exponential-ideal (λ x → holdsIsProp(p x))

∃̇ : {i : Level} {X : Set i} → (X → Prop) → Prop
∃̇ p = ₍ resize₁ ∥(Σ \x → p x holds)∥ ∥∥-isProp , resize₁-isProp ∥∥-isProp ₎

-- Introduction rules:

true-intro : true holds
true-intro = zero

∧-intro : {p q : Prop} → p holds → q holds → p ∧ q holds
∧-intro = _,_

∨-intro-L : {p q : Prop} → p holds → p ∨ q holds
∨-intro-L h = ∣ inl h ∣

∨-intro-R : {p q : Prop} → q holds → p ∨ q holds
∨-intro-R k = ∣ inr k ∣

⇒-intro : {p q : Prop} → (p holds → q holds) → (p ⇒ q holds)
⇒-intro = λ f → f

∃̇-intro : {X : U₀} {p : X → Prop} (x : X) → p x holds → ∃̇ p holds
∃̇-intro x h = ∣ x , h ∣

∀̇-intro : {X : U₀} {p : X → Prop} → ((x : X) → p x holds) → ∀̇ p holds
∀̇-intro = λ f → f

-- Elimination rules:

∧-elim-L : {p q : Prop} → p ∧ q holds → p holds
∧-elim-L = pr₁

∧-elim-R : {p q : Prop} → p ∧ q holds → q holds
∧-elim-R = pr₂

false-elim : {p : Prop} → false holds → p holds
false-elim = λ()

∨-elim : {p q r : Prop} → (p holds → r holds) → (q holds → r holds)
→ p ∨ q holds → r holds
∨-elim {p} {q} {r} f g = ∥∥-rec (holdsIsProp r) (+-rec f g)

⇒-elim : {p q : Prop} → (p holds → q holds) → p holds → q holds
⇒-elim = λ f → f

∃̇-elim : {i : Level} {X : U i} {p : X → Prop} {r : Prop} → ((x : X) → p x holds → r holds)
→ ∃̇ p holds → r holds
∃̇-elim {i} {X} {p} {r} f e = ∥∥-rec (holdsIsProp r) (Σ-rec f) (resize₁-out ∥∥-isProp e)

∀̇-elim : {X : U₀} {p : X → Prop} → ∀̇ p holds → (x : X) → p x holds
∀̇-elim = λ f → f

-- Characterizations in terms of _⇒_ and ∀̇:

false-charac : false ≡ ∀̇ \r → r
false-charac = propext a b
where
a : false holds → (∀̇ \r → r) holds
a = false-elim {(∀̇ \r → r)}
b : (∀̇ \r → r) holds → false holds
b φ = φ false

∧-charac : (p q : Prop) → p ∧ q ≡ ∀̇ \r → (p ⇒ q ⇒ r) ⇒ r
∧-charac p q = propext a b
where
a : p ∧ q holds → (∀̇ \r → (p ⇒ q ⇒ r) ⇒ r) holds
a pq = λ r pqr → pqr (∧-elim-L {p} {q} pq) (∧-elim-R {p} {q} pq)
b : (∀̇ \r → (p ⇒ q ⇒ r) ⇒ r) holds → p ∧ q holds
b φ = ∧-intro {p} {q} (φ p (λ x y → x)) (φ q (λ x y → y))

∨-charac : (p q : Prop) → p ∨ q ≡ ∀̇ \r → (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
∨-charac p q = propext a b
where
a : p ∨ q holds → (∀̇ \r → (p ⇒ r) ⇒ (q ⇒ r) ⇒ r) holds
a pq = λ r pr qr → ∨-elim {p} {q} {r} pr qr pq
b : (∀̇ \r → (p ⇒ r) ⇒ (q ⇒ r) ⇒ r) holds → p ∨ q holds
b φ = λ r f → φ r (λ x → f (inl x)) (λ y → f (inr y))

∃̇-charac : {i : Level} {X : U i} (p : X → Prop) → ∃̇ p ≡ ∀̇ \r → (∀̇ \x → p x ⇒ r) ⇒ r
∃̇-charac {i} {X} p = propext a b
where
a : (∃̇ p) holds → (∀̇ \r → (∀̇ \x → (p x ⇒ r)) ⇒ r) holds
a ep = λ r f → ∃̇-elim {i} {X} {p} {r} (λ x px → f x px) ep
b : (∀̇ \r → (∀̇ \x → (p x ⇒ r)) ⇒ r) holds → (∃̇ p) holds
b φ = λ r f → φ r (λ x px → f (x , px))
```