Ayberk Tosun, 10 March 2021.

Based in part by the `Cubical.Functions.Logic` module UF.of
`agda/cubical`.

\begin{code}

{-# OPTIONS --safe --without-K --exact-split #-}

module UF.Logic where

open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.SubtypeClassifier
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

\end{code}

\section{Conjunction}

\begin{code}

module Conjunction where

 _∧_ : Ω 𝓤 → Ω 𝓥 → Ω (𝓤 ⊔ 𝓥)
 P ∧ Q = (P holds × Q holds) , γ
  where
   γ = ×-is-prop (holds-is-prop P) (holds-is-prop Q)

 infixr  _∧_

\end{code}

\section{Universal quantification}

\begin{code}

module Universal (fe : Fun-Ext) where

 ∀[꞉]-syntax : (I : 𝓤 ̇ )→ (I → Ω 𝓥) → Ω (𝓤 ⊔ 𝓥)
 ∀[꞉]-syntax I P = ((i : I) → P i holds) , γ
  where
   γ : is-prop ((i : I) → P i holds)
   γ = Π-is-prop fe (holds-is-prop ∘ P)


 ∀[]-syntax : {I : 𝓤 ̇ } → (I → Ω 𝓥) → Ω (𝓤 ⊔ 𝓥)
 ∀[]-syntax {I = I} P = ∀[꞉]-syntax I P

 infixr -1 ∀[꞉]-syntax
 infixr -1 ∀[]-syntax

 syntax ∀[꞉]-syntax I (λ i → e) = Ɐ i ꞉ I , e
 syntax ∀[]-syntax    (λ i → e) = Ɐ i , e

\end{code}

\section{Implication}

\begin{code}

module Implication (fe : Fun-Ext) where

 open Universal fe

 infixr  _⇒_

 _⇒_ : Ω 𝓤 → Ω 𝓥 → Ω (𝓤 ⊔ 𝓥)
 P ⇒ Q = (P holds → Q holds) , γ
  where
   γ : is-prop (P holds → Q holds)
   γ = Π-is-prop fe λ _ → holds-is-prop Q

 open Conjunction

 _↔_ : Ω 𝓤 → Ω 𝓥 → Ω (𝓤 ⊔ 𝓥)
 P ↔ Q = (P ⇒ Q) ∧ (Q ⇒ P)

 infixr  _↔_

\end{code}

\section{Disjunction}

\begin{code}

module Disjunction (pt : propositional-truncations-exist) where

 open propositional-truncations-exist pt

 _∨_ : Ω 𝓤 → Ω 𝓥 → Ω (𝓤 ⊔ 𝓥)
 P ∨ Q = ∥ P holds + Q holds ∥ , ∥∥-is-prop

 infix  _∨_

\end{code}

\section{Truncation}

\begin{code}
module Truncation (pt : propositional-truncations-exist) where

  open PropositionalTruncation pt

  ∥_∥Ω : 𝓤 ̇  → Ω 𝓤
  ∥ A ∥Ω = ∥ A ∥ , ∥∥-is-prop

  ∥∥Ω-rec : {X : 𝓤  ̇} {P : Ω 𝓥} → (X → P holds) → ∥ X ∥ → P holds
  ∥∥Ω-rec {𝓤} {𝓥} {X} {P} = ∥∥-rec (holds-is-prop P)

\end{code}

\section{Existential quantification}

\begin{code}

module Existential (pt : propositional-truncations-exist) where

 open Truncation pt

 ∃[꞉]-syntax : (I : 𝓤 ̇ )→ (I → 𝓥 ̇ )→ Ω (𝓤 ⊔ 𝓥)
 ∃[꞉]-syntax I A = ∥ Σ i ꞉ I , A i ∥Ω

 ∃[]-syntax : {I : 𝓤 ̇ } → (I → 𝓥 ̇ )→ Ω (𝓤 ⊔ 𝓥)
 ∃[]-syntax {I = I} P = ∃[꞉]-syntax I P

 infixr -1 ∃[꞉]-syntax
 infixr -1 ∃[]-syntax

 syntax ∃[꞉]-syntax I (λ i → e) = Ǝ i ꞉ I , e
 syntax ∃[]-syntax    (λ i → e) = Ǝ i , e

\end{code}

\section{Negation of equality}

\begin{code}

module Negation-of-equality (fe : Fun-Ext) where

 _≢_ : {X : 𝓤 ̇ } → X → X → Ω 𝓤
 x ≢ y = (x ≠ y) , Π-is-prop fe (λ _ → 𝟘-is-prop)

\end{code}

\section{Propositional versions of subset operations}

\begin{code}

module PowersetOperations where

 open import UF.Powerset

 infix   _∈ₚ_

 _∈ₚ_ : {X : 𝓤  ̇} → X → (X → Ω 𝓥) → Ω 𝓥
 x ∈ₚ A = A x

\end{code}

\section{A module for importing all combinators}

\begin{code}

module AllCombinators
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
       where

 open Conjunction             public
 open Universal            fe public
 open Implication          fe public
 open Disjunction          pt public
 open Existential          pt public
 open Truncation           pt public
 open Negation-of-equality fe public
 open PowersetOperations      public

\end{code}