-- 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 : L} β†’ Prp i
true = ₍ πŸ™ , πŸ™-isProp β‚Ž

false : {i : L} β†’ Prp i
false = ₍ 𝟘 , 𝟘-isProp β‚Ž

holdsβ†’equal-true : {i : L} {p : Prp i} β†’ p holds β†’ p ≑ true
holdsβ†’equal-true {i} {p} h = Prp-≑ (prop-ua (holdsIsProp p) (holdsIsProp true) (Ξ» _ β†’ zero) (Ξ» _ β†’ h))

equal-trueβ†’holds : {i : L} {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 42 _β‡’_
infixr 41 _∨_
infixr 40 _∧_

_∧_ _∨_ _β‡’_ : {i : L} β†’ 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 : L} β†’ {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 : L} β†’ true {i} holds
true-intro = zero

∧-intro : {i : L} {p q : Prp i} β†’ p holds β†’ q holds β†’ p ∧ q holds
∧-intro = _,_

∨-intro-L : {i : L} {p q : Prp i} β†’ p holds β†’ p ∨ q holds
∨-intro-L h = ∣ inl h ∣

∨-intro-R : {i : L} {p q : Prp i} β†’ q holds β†’ p ∨ q holds
∨-intro-R k = ∣ inr k ∣

β‡’-intro : {i : L} {p q : Prp i} β†’ (p holds β†’ q holds) β†’ p β‡’ q holds
β‡’-intro = Ξ» f β†’ f

βˆƒΜ‡-intro : {i j : L} {X : U i} {p : X β†’ Prp j} (x : X) β†’ p x holds β†’ βˆƒΜ‡ p holds
βˆƒΜ‡-intro x h = ∣ x , h ∣

βˆ€Μ‡-intro : {i j : L} {X : U i} {p : X β†’ Prp j} β†’ ((x : X) β†’ p x holds) β†’ βˆ€Μ‡ p holds
βˆ€Μ‡-intro = Ξ» f β†’ f

-- Elimination principles:

∧-elim-L :  {i : L} {p q : Prp i} β†’ p ∧ q holds β†’ p holds
∧-elim-L = pr₁

∧-elim-R :  {i : L} {p q : Prp i} β†’ p ∧ q holds β†’ q holds
∧-elim-R = prβ‚‚

false-elim : {i j : L} {p : Prp i} β†’ false {j} holds β†’ p holds
false-elim = Ξ»()

∨-elim :  {i : L} {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 : L} {p q : Prp i} β†’ (p holds β†’ q holds) β†’ p holds β†’ q holds
β‡’-elim = Ξ» f β†’ f

βˆƒΜ‡-elim : {i j : L} {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 : L} {X : U i} {p : X β†’ Prp j} β†’ βˆ€Μ‡ p holds β†’ (x : X) β†’ p x holds
βˆ€Μ‡-elim = Ξ» f β†’ f

-- Characterizations in terms of _β‡’_ and βˆ€Μ‡:

_⟷_ : {i j : Level} β†’ Prp i β†’ Prp j β†’ U (i βŠ” j)
p ⟷ q = (p holds β†’ q holds) Γ— (q holds β†’ p holds)

infix 32 _⟷_

false-charac : {i : L} β†’ (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 : L} (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 : L} (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 : L} {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)))