-- Various functions for manipulating hProps.
--
-- This file used to be part of Foundations, but it turned out to be
-- not very useful so moved here. Feel free to upstream content.
--
-- Note that it is often a bad idea to use hProp instead of having the
-- isProp proof separate. The reason is that Agda can rarely infer
-- isProp proofs making it easier to just give them explicitly instead
-- of having them bundled up with the type.
--
{-# OPTIONS --safe #-}
module Cubical.Functions.Logic where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Function
open import Cubical.Foundations.Univalence using (hPropExt)

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.HITs.PropositionalTruncation as PropTrunc

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


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

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 ⇐∶_⇒∶_

∥_∥ₚ : Type   hProp 
 A ∥ₚ =  A ∥₁ , isPropPropTrunc

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

hProp≡ :  P    Q   P  Q
hProp≡ = TypeOfHLevel≡ 1

isProp⟨⟩ : (A : hProp )  isProp  A 
isProp⟨⟩ = snd

--------------------------------------------------------------------------------
-- 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≡ (hPropExt (isProp⟨⟩ P) (isProp⟨⟩ Q) P⇒Q Q⇒P)

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)

⇔-id : (P : hProp )   P  P 
⇔-id P = (idfun  P ) , (idfun  P )

--------------------------------------------------------------------------------
-- 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) ∣₁ = isPropPropTrunc (assoc2  ⊎.inl x ∣₁) (assoc2  ⊎.inl y ∣₁) i
    assoc2 (squash₁ x y i)             = isPropPropTrunc (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)