-- 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)))