-- Martin Escardo, 7th August 2015.

{-# OPTIONS --without-K #-}

module logic where

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

-- The two canonical truth values:

true : {i : 𝕃}  Prop{i}
true = ( 𝟙 , 𝟙-isProp )

false : {i : 𝕃}  Prop{i}
false = ( 𝟘 , 𝟘-isProp )

holds→equal-true : {i : 𝕃} {p : Prop{i}}  p holds  p  true
holds→equal-true {i} {p} h = Prop-≡ (prop-ua (holdsIsProp p) (holdsIsProp true)  _  zero)  _  h))

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

-- The logical connectives:

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

_∧_ _∨_ _⇒_ : {i : 𝕃}  Prop{i}  Prop{i}  Prop{i}

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 j : 𝕃}  {X : U i}  (X  Prop{j})  Prop{i  j}

∀̇ p = ( (∀ x  p x holds) , isProp-exponential-ideal  x  holdsIsProp(p x)) )

∃̇ p = ( (Σ \x  p x holds) , ∥∥-isProp )

-- Introduction principles:

true-intro : {i : 𝕃}  true {i} holds
true-intro = zero

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

∨-intro-L : {i : 𝕃} {p q : Prop{i}}  p holds  p  q holds
∨-intro-L h =  inl h 

∨-intro-R : {i : 𝕃} {p q : Prop{i}}  q holds  p  q holds
∨-intro-R k =  inr k 

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

∃̇-intro : {i j : 𝕃} {X : U i} {p : X  Prop{j}} (x : X)  p x holds  ∃̇ p holds
∃̇-intro x h =  x , h 

∀̇-intro : {i j : 𝕃} {X : U i} {p : X  Prop{j}}  ((x : X)  p x holds)  ∀̇ p holds
∀̇-intro = λ f  f

-- Elimination principles:

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

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

false-elim : {i j : 𝕃} {p : Prop{i}}  false {j} holds  p holds
false-elim = λ()

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

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

∃̇-elim : {i j : 𝕃} {X : U i} {p : X  Prop{j}} {r : Prop{i  j}} 
         ((x : X)  p x holds  r holds) 
         ∃̇ p holds  r holds 
∃̇-elim {i} {j} {X} {p} {r} f = ∥∥-rec (holdsIsProp r) (Σ-rec f)

∀̇-elim : {i j : 𝕃} {X : U i} {p : X  Prop{j}}  ∀̇ p holds  (x : X)  p x holds
∀̇-elim = λ f  f

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

_⟷_ : {i j : 𝕃}  Prop{i}  Prop{j}  U (i  j)
p  q = (p holds  q holds) × (q holds  p holds)

infix 32 _⟷_

false-charac : {i : 𝕃}  (false {i})  ∀̇ \r  r
false-charac {i} = (a , b)
 where
  a : false holds  (∀̇ \r  r) holds
  a = false-elim {lsuc i} {i} {(∀̇ \r  r)}
  b : (∀̇ \r  r) holds  false holds
  b φ = φ false

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

∨-charac : {i : 𝕃} (p q : Prop{i})  (p  q)  ∀̇ \r  (p  r)  (q  r)  r
∨-charac {i} p q = (a , b)
 where
   a : p  q holds  (∀̇ \r  (p  r)  (q  r)  r) holds
   a pq = λ r pr qr  ∨-elim {i} {p} {q} {r} pr qr pq
   b : (∀̇ \r  (p  r)  (q  r)  r) holds  p  q holds
   b φ = decrease  r f  φ r  x  f (inl x))  y  f (inr y))) 

∃̇-charac : {i : 𝕃} {X : U i} (p : X  Prop{i}) 
          ∃̇ p  ∀̇ \r  (∀̇ \x  p x  r)  r 
∃̇-charac {i} {X} p = (a , b)
 where
  a : (∃̇ p) holds  (∀̇ \r  (∀̇ \x  (p x  r))  r) holds 
  a ep = λ r f  ∃̇-elim {i} {i} {X} {p} {r}  x px  f x px) ep
  b : (∀̇ \r  (∀̇ \x  (p x  r))  r) holds  (∃̇ p) holds 
  b φ = decrease  r f  φ r  x px  f (x , px)))