```-- 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 : π} β Prp{i}
true = ( π , π-isProp )

false : {i : π} β Prp{i}
false = ( π , π-isProp )

holdsβequal-true : {i : π} {p : Prp{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 : Prp{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 : π} β Prp{i} β Prp{i} β Prp{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 β Prp{j}) β Prp{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 : Prp{i}} β p holds β q holds β p β§ q holds
β§-intro = _,_

β¨-intro-L : {i : π} {p q : Prp{i}} β p holds β p β¨ q holds
β¨-intro-L h = β£ inl h β£

β¨-intro-R : {i : π} {p q : Prp{i}} β q holds β p β¨ q holds
β¨-intro-R k = β£ inr k β£

β-intro : {i : π} {p q : Prp{i}} β (p holds β q holds) β p β q holds
β-intro = Ξ» f β f

βΜ-intro : {i j : π} {X : U i} {p : X β Prp{j}} (x : X) β p x holds β βΜ p holds
βΜ-intro x h = β£ x , h β£

βΜ-intro : {i j : π} {X : U i} {p : X β Prp{j}} β ((x : X) β p x holds) β βΜ p holds
βΜ-intro = Ξ» f β f

-- Elimination principles:

β§-elim-L :  {i : π} {p q : Prp{i}} β p β§ q holds β p holds
β§-elim-L = prβ

β§-elim-R :  {i : π} {p q : Prp{i}} β p β§ q holds β q holds
β§-elim-R = prβ

false-elim : {i j : π} {p : Prp{i}} β false {j} holds β p holds
false-elim = Ξ»()

β¨-elim :  {i : π} {p q r : Prp{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 : Prp{i}} β (p holds β q holds) β p holds β q holds
β-elim = Ξ» f β f

βΜ-elim : {i j : π} {X : U i} {p : X β Prp{j}} {r : Prp{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 β Prp{j}} β βΜ p holds β (x : X) β p x holds
βΜ-elim = Ξ» f β f

-- Characterizations in terms of _β_ and βΜ:

_β·_ : {i j : π} β Prp{i} β Prp{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 : Prp{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 : Prp{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 β Prp{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)))
```