{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Foundations.Logic where

import Cubical.Data.Empty as 
open import Cubical.Data.Sum as  using (_⊎_)
open import Cubical.Data.Unit
open import Cubical.Data.Sigma

open import Cubical.Foundations.Prelude as FP
open import Cubical.Functions.Embedding
open import Cubical.Functions.Fibration as Fib
open import Cubical.Foundations.Equiv

open import Cubical.HITs.PropositionalTruncation as PropTrunc

open import Cubical.Foundations.HLevels using (hProp; isPropΠ; isPropΠ2; isSetΠ; isSetHProp; isOfHLevelΣ; isPropΣ) public
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Univalence using (ua)

open import Cubical.Relation.Nullary hiding (¬_)

infix 10 ¬_
infixr 8 _⊔_
infixr 8 _⊔′_
infixr 8 _⊓_
infixr 8 _⊓′_
infixr 6 _⇒_
infixr 4 _⇔_
infix 30 _≡ₚ_
infix 30 _≢ₚ_

infix 2 ∃[]-syntax
infix 2 ∃[∶]-syntax

infix 2 ∀[∶]-syntax
infix 2 ∀[]-syntax

infix 2 ⇒∶_⇐∶_
infix 2 ⇐∶_⇒∶_

--------------------------------------------------------------------------------
-- The type hProp of mere propositions
-- the definition hProp is given in Foundations.HLevels
-- hProp ℓ = Σ (Type ℓ) isProp

private
  variable
     ℓ' ℓ'' : Level
    P Q R : hProp 
    A B C : Type 

[_] : hProp   Type 
[_] = fst

isProp[] : (A : hProp )  isProp [ A ]
isProp[] = snd

∥_∥ₚ : Type   hProp 
 A ∥ₚ =  A  , propTruncIsProp

_≡ₚ_ : (x y : A)  hProp _
x ≡ₚ y =  x  y ∥ₚ

hProp≡ : [ P ]  [ Q ]  P  Q
hProp≡ p = Σ≡Prop (\ _  isPropIsProp) p

--------------------------------------------------------------------------------
-- Logical implication of mere propositions

_⇒_ : (A : hProp )  (B : hProp ℓ')  hProp _
A  B = ([ A ]  [ B ]) , isPropΠ λ _  isProp[] B

⇔toPath : [ P  Q ]  [ Q  P ]  P  Q
⇔toPath {P = P} {Q = Q} P⇒Q Q⇒P = hProp≡ (isoToPath
  (iso P⇒Q Q⇒P  b  isProp[] Q (P⇒Q (Q⇒P b)) b) λ a  isProp[] P (Q⇒P (P⇒Q a)) a))

pathTo⇒ : P  Q  [ P  Q ]
pathTo⇒ p x = subst fst  p x

pathTo⇐ : P  Q  [ Q  P ]
pathTo⇐ p x = subst fst (sym p) x

substₚ : {x y : A} (B : A  hProp )  [ x ≡ₚ y  B x  B y ]
substₚ {x = x} {y = y} B = PropTrunc.elim  _  isPropΠ λ _  isProp[] (B y)) (subst (fst  B))

--------------------------------------------------------------------------------
-- Mixfix notations for ⇔-toPath
-- see ⊔-identityˡ and ⊔-identityʳ for the difference

⇒∶_⇐∶_ : [ P  Q ]  [ Q  P ]  P  Q
⇒∶_⇐∶_ = ⇔toPath

⇐∶_⇒∶_ : [ Q  P ]  [ P  Q ]  P  Q
⇐∶ g ⇒∶ f  = ⇔toPath f g
--------------------------------------------------------------------------------
-- False and True

 : hProp _
 = ⊥.⊥ , λ ()

 : hProp _
 = Unit ,  _ _ _  tt)

--------------------------------------------------------------------------------
-- Pseudo-complement of mere propositions

¬_ : hProp   hProp _
¬ A = ([ A ]  ⊥.⊥) , isPropΠ λ _  ⊥.isProp⊥

_≢ₚ_ : (x y : A)  hProp _
x ≢ₚ y = ¬ x ≡ₚ y

--------------------------------------------------------------------------------
-- Disjunction of mere propositions

_⊔′_ : Type   Type ℓ'  Type _
A ⊔′ B =  A  B 

_⊔_ : hProp   hProp ℓ'  hProp _
P  Q =  [ P ]  [ Q ] ∥ₚ

inl : A  A ⊔′ B
inl x =  ⊎.inl x 

inr : B  A ⊔′ B
inr x =  ⊎.inr x 

⊔-elim : (P : hProp ) (Q : hProp ℓ') (R : [ P  Q ]  hProp ℓ'')
   (∀ x  [ R (inl x) ])  (∀ y  [ R (inr y) ])  (∀ z  [ R z ])
⊔-elim _ _ R P⇒R Q⇒R = PropTrunc.elim (snd  R) (⊎.elim P⇒R Q⇒R)

--------------------------------------------------------------------------------
-- Conjunction of mere propositions
_⊓′_ : Type   Type ℓ'  Type _
A ⊓′ B = A × B

_⊓_ : hProp   hProp ℓ'  hProp _
A  B = [ A ] ⊓′ [ B ] , isOfHLevelΣ 1 (isProp[] A) (\ _  isProp[] B)

⊓-intro : (P : hProp ) (Q : [ P ]  hProp ℓ') (R : [ P ]  hProp ℓ'')
        (∀ a  [ Q a ])  (∀ a  [ R a ])  (∀ (a : [ P ])  [ Q a  R a ] )
⊓-intro _ _ _ = \ f g a  f a , g a

--------------------------------------------------------------------------------
-- Logical bi-implication of mere propositions

_⇔_ : hProp   hProp ℓ'  hProp _
A  B = (A  B)  (B  A)

--------------------------------------------------------------------------------
-- Universal Quantifier


∀[∶]-syntax : (A  hProp )  hProp _
∀[∶]-syntax {A = A} P = (∀ x  [ P x ]) , isPropΠ (isProp[]  P)

∀[]-syntax : (A  hProp )  hProp _
∀[]-syntax {A = A} P = (∀ x  [ P x ]) , isPropΠ (isProp[]  P)

syntax ∀[∶]-syntax {A = A}  a  P) = ∀[ a  A ] P
syntax ∀[]-syntax  a  P)          = ∀[ a ] P
--------------------------------------------------------------------------------
-- Existential Quantifier


∃[]-syntax : (A  hProp )  hProp _
∃[]-syntax {A = A} P =  Σ A ([_]  P) ∥ₚ

∃[∶]-syntax : (A  hProp )  hProp _
∃[∶]-syntax {A = A} P =  Σ A ([_]  P) ∥ₚ

syntax ∃[∶]-syntax {A = A}  x  P) = ∃[ x  A ] P
syntax ∃[]-syntax  x  P) = ∃[ x ] P
--------------------------------------------------------------------------------
-- Decidable mere proposition

Decₚ : (P : hProp )  hProp 
Decₚ P = Dec [ P ] , isPropDec (isProp[] P)

--------------------------------------------------------------------------------
-- Negation commutes with truncation

∥¬A∥≡¬∥A∥ : (A : Type )   (A  ⊥.⊥) ∥ₚ  (¬  A ∥ₚ)
∥¬A∥≡¬∥A∥ _ =
  ⇒∶  ¬A A  PropTrunc.elim  _  ⊥.isProp⊥)
    (PropTrunc.elim  _  isPropΠ λ _  ⊥.isProp⊥)  ¬p p  ¬p p) ¬A) A)
  ⇐∶ λ ¬p    p  ¬p  p ) 

--------------------------------------------------------------------------------
-- (hProp, ⊔, ⊥) is a bounded ⊔-semilattice

⊔-assoc : (P : hProp ) (Q : hProp ℓ') (R : hProp ℓ'')
   P  (Q  R)  (P  Q)  R
⊔-assoc P Q R =
  ⇒∶ ⊔-elim P (Q  R)  _  (P  Q)  R)
    (inl  inl)
    (⊔-elim Q R  _  (P  Q)  R) (inl  inr) inr)

  ⇐∶ assoc2
  where
    assoc2 : (A ⊔′ B) ⊔′ C  A ⊔′ (B ⊔′ C)
    assoc2  ⊎.inr a               =  ⊎.inr  ⊎.inr a  
    assoc2  ⊎.inl  ⊎.inr b    =  ⊎.inr  ⊎.inl b  
    assoc2  ⊎.inl  ⊎.inl c    =  ⊎.inl c 
    assoc2  ⊎.inl (squash x y i)  = propTruncIsProp (assoc2  ⊎.inl x ) (assoc2  ⊎.inl y ) i
    assoc2 (squash x y i)             = propTruncIsProp (assoc2 x) (assoc2 y) i

⊔-idem : (P : hProp )  P  P  P
⊔-idem P =
  ⇒∶ (⊔-elim P P (\ _  P) (\ x  x) (\ x  x))
  ⇐∶ inl

⊔-comm : (P : hProp ) (Q : hProp ℓ')  P  Q  Q  P
⊔-comm P Q =
  ⇒∶ (⊔-elim P Q (\ _  (Q  P)) inr inl)
  ⇐∶ (⊔-elim Q P (\ _  (P  Q)) inr inl)

⊔-identityˡ : (P : hProp )    P  P
⊔-identityˡ P =
  ⇒∶ (⊔-elim  P  _  P)  ())  x  x))
  ⇐∶ inr

⊔-identityʳ : (P : hProp )  P    P
⊔-identityʳ P = ⇔toPath (⊔-elim P   _  P)  x  x) λ ()) inl

--------------------------------------------------------------------------------
-- (hProp, ⊓, ⊤) is a bounded ⊓-lattice

⊓-assoc : (P : hProp ) (Q : hProp ℓ') (R : hProp ℓ'')
   P  Q  R  (P  Q)  R
⊓-assoc _ _ _ =
  ⇒∶  {(x , (y , z))   (x , y) , z})
  ⇐∶  {((x , y) , z)  x , (y , z) })

⊓-comm : (P : hProp ) (Q : hProp ℓ')  P  Q  Q  P
⊓-comm _ _ = ⇔toPath (\ p  p .snd , p .fst) (\ p  p .snd , p .fst)

⊓-idem : (P : hProp )  P  P  P
⊓-idem _ = ⇔toPath fst  x  x , x)

⊓-identityˡ : (P : hProp )    P  P
⊓-identityˡ _ = ⇔toPath snd λ x  tt , x

⊓-identityʳ : (P : hProp )  P    P
⊓-identityʳ _ = ⇔toPath fst λ x  x , tt

--------------------------------------------------------------------------------
-- Distributive laws

⇒-⊓-distrib : (P : hProp ) (Q : hProp ℓ')(R : hProp ℓ'')
   P  (Q  R)  (P  Q)  (P  R)
⇒-⊓-distrib _ _ _ =
  ⇒∶  f  (fst  f) , (snd  f))
  ⇐∶  { (f , g) x  f x , g x})

⊓-⊔-distribˡ : (P : hProp ) (Q : hProp ℓ')(R : hProp ℓ'')
   P  (Q  R)  (P  Q)  (P  R)
⊓-⊔-distribˡ P Q R =
  ⇒∶  { (x , a)  ⊔-elim Q R  _  (P  Q)  (P  R))
         y   ⊎.inl (x , y)  )
         z   ⊎.inr (x , z)  ) a })

  ⇐∶ ⊔-elim (P  Q) (P  R)  _  P  Q  R)
        y  fst y , inl (snd y))
        z  fst z , inr (snd z))

⊔-⊓-distribˡ : (P : hProp ) (Q : hProp ℓ')(R : hProp ℓ'')
   P  (Q  R)  (P  Q)  (P  R)
⊔-⊓-distribˡ P Q R =
  ⇒∶ ⊔-elim P (Q  R)  _  (P  Q)  (P  R) )
    (\ x  inl x , inl x) (\ p  inr (p .fst) , inr (p .snd))

  ⇐∶  { (x , y)  ⊔-elim P R  _  P  Q  R) inl
       z  ⊔-elim P Q  _  P  Q  R) inl  y  inr (y , z)) x) y })

⊓-∀-distrib :  (P : A  hProp ) (Q : A  hProp ℓ')
   (∀[ a  A ] P a)  (∀[ a  A ] Q a)  (∀[ a  A ] (P a  Q a))
⊓-∀-distrib P Q =
  ⇒∶  {(p , q) a  p a , q a})
  ⇐∶ λ pq  (fst  pq ) , (snd  pq)

--------------------------------------------------------------------------------
-- Introduce the "powerset" of a type in the style of Escardó's lecture notes:
-- https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#propositionalextensionality

 :  {}  Type   Type (ℓ-suc )
 {} X = X  hProp 

infix 5 _∈_
_∈_ : {X : Type }  X   X  Type 
x  A = [ A x ]

_⊆_ : {X : Type }   X   X  Type 
A  B =  x  x  A  x  B

∈-isProp : {X : Type } (A :  X) (x : X)  isProp (x  A)
∈-isProp A = isProp[]  A

⊆-isProp : {X : Type } (A B :  X)  isProp (A  B)
⊆-isProp A B = isPropΠ2  x _  ∈-isProp B x)

⊆-refl : {X : Type } (A :  X)  A  A
⊆-refl A x = idfun (x  A)


⊆-refl-consequence : {X : Type } (A B :  X)
                    A  B  (A  B) × (B  A)
⊆-refl-consequence {X} A B p = subst  B  (A  B)) p (⊆-refl A) , subst  A  (B  A)) (sym p) (⊆-refl B)


⊆-extensionality : {X : Type } (A B :  X)
                  (A  B) × (B  A)  A  B
⊆-extensionality A B (φ , ψ) i x = ⇔toPath {P = (A x)} {Q = (B x)} (φ x) (ψ x) i


powersets-are-sets : {X : Type }  isSet ( X)
powersets-are-sets {X = X} = isSetΠ  _  isSetHProp)

⊆-extensionalityEquiv : {X : Type } (A B :  X)
                       (A  B) × (B  A)  (A  B)
⊆-extensionalityEquiv A B = isoToEquiv (iso (⊆-extensionality A B)
                                            (⊆-refl-consequence A B)
                                             _  powersets-are-sets A B _ _)
                                             _  isPropΣ (⊆-isProp A B)  _  ⊆-isProp B A) _ _))


-- We show that the powerset is the subtype classifier
-- i.e. ℙ X ≃ Σ[A ∈ Type ℓ] (A ↪ X)
Embedding→Subset : {X : Type }  Σ[ A  Type  ] (A  X)   X
Embedding→Subset (_ , f , isPropFiber) x = fiber f x , isPropFiber x

Subset→Embedding : {X : Type }   X  Σ[ A  Type  ] (A  X)
Subset→Embedding {X = X} A = D , f , ψ
 where
  D = Σ[ x  X ] x  A

  f : D  X
  f d = d .fst

  ψ : hasPropFibers f
  ψ x ((y , y∈A) , y≡x) ((z , z∈A) , z≡x) = ΣPathP (r , q)
   where
    p : y  z
    p = y≡x  sym z≡x

    r : (y , y∈A)  (z , z∈A)
    r = Σ≡Prop (∈-isProp A) p

    q : PathP  i  p i  x) y≡x z≡x
    q i j = hcomp  k  λ { (j = i1)  x
                           ; (i = i0)  y≡x j
                           ; (i = i1)  z≡x (~ k  j) })
                  (y≡x (i  j))


Subset→Embedding→Subset : {X : Type }  section (Embedding→Subset {} {X}) (Subset→Embedding {} {X})
Subset→Embedding→Subset _ = funExt λ x  Σ≡Prop  _  FP.isPropIsProp) (ua (Fib.FiberIso.fiberEquiv _ x))

Embedding→Subset→Embedding : {X : Type }  retract (Embedding→Subset {} {X}) (Subset→Embedding {} {X})
Embedding→Subset→Embedding { = } {X = X} (A , f , ψ) = cong (Σ-assoc-≃ .fst) p
 where
 χ = Subset→Embedding (Embedding→Subset (A , f , ψ)) .snd .snd

 p : (((Σ[ x  X ] fiber f x) , fst) , χ)  ((A , f) , ψ)
 p = Σ≡Prop  _  hasPropFibersIsProp) ((equivToIso (Fib.fibrationEquiv X )) .Iso.leftInv (A , f))




Subset≃Embedding : {X : Type }   X  (Σ[ A  Type  ] (A  X))
Subset≃Embedding = isoToEquiv (iso Subset→Embedding Embedding→Subset Embedding→Subset→Embedding Subset→Embedding→Subset)

Subset≡Embedding : {X : Type }   X  (Σ[ A  Type  ] (A  X))
Subset≡Embedding = ua Subset≃Embedding