---
title:        Logic
author:       MartΓ­n EscardΓ³ and Ayberk Tosun
date-started: 2021-03-10
---

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

\begin{code}

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

module UF.Logic where

open import MLTT.Spartan
open import UF.Equiv
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier
open import UF.SubtypeClassifier-Properties
open import UF.Sets

\end{code}

\section{Negation}

\begin{code}

module Negation (fe : funext 𝓀 𝓀₀) where

 ⇁_ : Ξ© 𝓀 β†’ Ξ© 𝓀
 ⇁_ = not fe

 ⇁⇁_ : Ξ© 𝓀 β†’ Ξ© 𝓀
 ⇁⇁ p = ⇁(⇁ p)

\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 4 _∧_

\end{code}

Added by Martin Escardo 1st Nov 2023.

\begin{code}

 ∧-Intro :  (p : Ξ© 𝓀) (q : Ξ© π“₯) β†’ p holds β†’ q holds β†’ (p ∧ q) holds
 ∧-Intro p q a b = (a , b)

 ∧-Elim-L : (p : Ξ© 𝓀) (q : Ξ© π“₯) β†’ (p ∧ q) holds β†’ p holds
 ∧-Elim-L p q = pr₁

 ∧-Elim-R :  (p : Ξ© 𝓀) (q : Ξ© π“₯) β†’ (p ∧ q) holds β†’ q holds
 ∧-Elim-R p q = prβ‚‚

 module _ (pe : propext 𝓀) (fe : funext 𝓀 𝓀) where

  ∧-intro :  (p q : Ξ© 𝓀) β†’ p ＝ ⊀ β†’ q ＝ ⊀ β†’ p ∧ q ＝ ⊀
  ∧-intro p q a b = holds-gives-equal-⊀ pe fe (p ∧ q)
                     (∧-Intro p q
                       (equal-⊀-gives-holds p a)
                       (equal-⊀-gives-holds q b))

  ∧-elim-L :  (p q : Ξ© 𝓀) β†’ p ∧ q ＝ ⊀ β†’ p ＝ ⊀
  ∧-elim-L p q c = holds-gives-equal-⊀ pe fe p
                    (∧-Elim-L p q (equal-⊀-gives-holds (p ∧ q) c))

  ∧-elim-R :  (p q : Ξ© 𝓀) β†’ p ∧ q ＝ ⊀ β†’ q ＝ ⊀
  ∧-elim-R p q c = holds-gives-equal-⊀ pe fe q
                    (∧-Elim-R p q (equal-⊀-gives-holds (p ∧ q) c))

\end{code}

Added by Martin Escardo 8th September 2025.

\begin{code}

 module _ (pe : propext 𝓀)
          (fe : funext 𝓀 𝓀)
        where

  ⊀-is-∧-left-neutral : (p : Ξ© 𝓀) β†’ ⊀ {𝓀} ∧ p ＝ p
  ⊀-is-∧-left-neutral p =
   Ξ©-extensionality pe fe
    prβ‚‚
    (Ξ» p-holds β†’ ⋆ , p-holds)

  ⊀-is-∧-right-neutral : (p : Ξ© 𝓀) β†’ p ∧ ⊀ {𝓀} ＝ p
  ⊀-is-∧-right-neutral p =
   Ξ©-extensionality pe fe
    pr₁
    (Ξ» p-holds β†’ p-holds , ⋆)

  βŠ₯-is-∧-left-absorbtive : (p : Ξ© 𝓀) β†’ βŠ₯ {𝓀} ∧ p ＝ βŠ₯
  βŠ₯-is-∧-left-absorbtive p =
   Ξ©-extensionality pe fe
    pr₁
    𝟘-elim

  ∧-is-idempotent : (p : Ξ© 𝓀) β†’ p ∧ p ＝ p
  ∧-is-idempotent p =
   Ξ©-extensionality pe fe
    pr₁
    (Ξ» p-holds β†’ p-holds , p-holds)

\end{code}

TODO. Add all the semilattice equations.

End of addition.

\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

 βˆ€β‚‚[κž‰]-syntax : (I : 𝓀 Μ‡ )β†’ (I β†’ I β†’ Ξ© π“₯) β†’ Ξ© (𝓀 βŠ” π“₯)
 βˆ€β‚‚[κž‰]-syntax I P = ((i j : I) β†’ P i j holds) , Ξ³
  where
   Ξ³ : is-prop ((i j : I) β†’ P i j holds)
   Ξ³ = Ξ β‚‚-is-prop fe Ξ» i j β†’ holds-is-prop (P i j)

 infixr -1 βˆ€β‚‚[κž‰]-syntax

 syntax βˆ€β‚‚[κž‰]-syntax I (Ξ» i j β†’ e) = β±― i j κž‰ I , e

 βˆ€β‚ƒ[κž‰]-syntax : (I : 𝓀 Μ‡ )β†’ (I β†’ I β†’ I β†’ Ξ© π“₯) β†’ Ξ© (𝓀 βŠ” π“₯)
 βˆ€β‚ƒ[κž‰]-syntax I P = β±― i κž‰ I , β±― j κž‰ I , β±― k κž‰ I , P i j k

 infixr -1 βˆ€β‚ƒ[κž‰]-syntax

 syntax βˆ€β‚ƒ[κž‰]-syntax I (Ξ» i j k β†’ e) = β±― i j k κž‰ I , e

\end{code}

\section{Implication}

\begin{code}

module Implication (fe : Fun-Ext) where

 open Universal fe

 infixr 3 _β‡’_

 _β‡’_ : Ξ© 𝓀 β†’ Ξ© π“₯ β†’ Ξ© (𝓀 βŠ” π“₯)
 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 3 _⇔_

 biimplication-forward : (P : Ξ© 𝓀) (Q : Ξ© π“₯)
                       β†’ (P ⇔ Q) holds β†’ (P β‡’ Q) holds
 biimplication-forward P Q (Ο† , _) = Ο†

 biimplication-backward : (P : Ξ© 𝓀) (Q : Ξ© π“₯)
                        β†’ (P ⇔ Q) holds β†’ (Q β‡’ P) holds
 biimplication-backward P Q (_ , ψ) = ψ

 infix 3 Β¬β‚š_

 Β¬β‚š_ : Ξ© 𝓀 β†’ Ξ© 𝓀
 Β¬β‚š_ {𝓀} P = P β‡’ βŠ₯ {𝓀}

 Β¬Β¬β‚š_ : Ξ© 𝓀 β†’ Ξ© 𝓀
 Β¬Β¬β‚š p = Β¬β‚š(Β¬β‚š p)

 Β¬Β¬Β¬β‚š_ : Ξ© 𝓀 β†’ Ξ© 𝓀
 Β¬Β¬Β¬β‚š p = Β¬β‚š(Β¬Β¬β‚š p)

\end{code}

Added by Martin Escardo 1st Nov 2023.

\begin{code}

 ⇔-gives-β‡’ = biimplication-forward
 ⇔-gives-⇐ = biimplication-backward

 module _ (pe : propext 𝓀) where

  ⊀-⇔-neutral : (p : Ξ© 𝓀) β†’ (p ⇔ ⊀) ＝ p
  ⊀-⇔-neutral p =
   Ξ©-extensionality pe fe
   (Ξ» (h : (p ⇔ ⊀ {𝓀}) holds) β†’ ⇔-gives-⇐ p ⊀ h ⊀-holds)
   (Ξ» (h : p holds) β†’ (Ξ» _ β†’ ⊀-holds) , (Ξ» _ β†’ h))

  ⇔-swap :  (p : Ξ© 𝓀) (q : Ξ© π“₯) β†’ (p ⇔ q) holds β†’ (q ⇔ p) holds
  ⇔-swap p q (h , k) = (k , h)

  ⇔-swap' :  (p q : Ξ© 𝓀) β†’ (p ⇔ q) ＝ ⊀ β†’ (q ⇔ p) ＝ ⊀
  ⇔-swap' p q e = holds-gives-equal-⊀ pe fe (q ⇔ p)
                   (⇔-swap p q (equal-⊀-gives-holds (p ⇔ q) e))

  ⇔-sym :  (p q : Ξ© 𝓀) β†’ (p ⇔ q) ＝ (q ⇔ p)
  ⇔-sym p q = Ξ©-ext pe fe (⇔-swap' p q) (⇔-swap' q p)

  ⊀-⇔-neutral' : (p : Ξ© 𝓀) β†’ (⊀ ⇔ p) ＝ p
  ⊀-⇔-neutral' p = (⊀ ⇔ p ＝⟨ ⇔-sym ⊀ p ⟩
                    p ⇔ ⊀ ＝⟨ ⊀-⇔-neutral p ⟩
                    p     ∎)

  ⇔-refl : (p : Ξ© 𝓀) β†’ (p ⇔ p) ＝ ⊀
  ⇔-refl p = holds-gives-equal-⊀ pe fe
              (p ⇔ p)
              (id , id)

  ＝-gives-⇔  :  (p q : Ξ© 𝓀) β†’  p ＝ q β†’ (p ⇔ q) ＝ ⊀
  ＝-gives-⇔ p p refl = ⇔-refl p

  ⇔-gives-＝ :  (p q : Ξ© 𝓀) β†’ (p ⇔ q) ＝ ⊀ β†’ p ＝ q
  ⇔-gives-＝ p q e = Ξ©-extensionality pe fe f g
   where
    f : p holds β†’ q holds
    f = ⇔-gives-β‡’ p q (equal-⊀-gives-holds (p ⇔ q) e)

    g : q holds β†’ p holds
    g = ⇔-gives-⇐ p q (equal-⊀-gives-holds (p ⇔ q) e)

  ⇔-equiv-to-＝ :  (p q : Ξ© 𝓀) β†’ ((p ⇔ q) ＝ ⊀) ≃ (p ＝ q)
  ⇔-equiv-to-＝ p q = qinveq
                       (⇔-gives-＝ p q)
                       (＝-gives-⇔ p q ,
                       (Ξ» _ β†’ Ξ©-is-set fe pe _ _) ,
                       (Ξ» _ β†’ Ξ©-is-set fe pe _ _))

\end{code}

Added by Martin Escardo 8th September 2025.

\begin{code}

  βŠ₯β‡’anything-is-⊀ : (p : Ξ© 𝓀) β†’ (βŠ₯ {𝓀} β‡’ p) ＝ ⊀ {𝓀}
  βŠ₯β‡’anything-is-⊀ p =
   Ξ©-extensionality pe fe
    (Ξ» (a : 𝟘 β†’ p holds) β†’ ⋆)
    (Ξ» ⋆ β†’ 𝟘-elim)

  βŠ€β‡’anything-is-the-thing : (p : Ξ© 𝓀) β†’ (⊀ {𝓀} β‡’ p) ＝ p
  βŠ€β‡’anything-is-the-thing p =
   Ξ©-extensionality pe fe
    (Ξ» (f : πŸ™ β†’ p holds) β†’ f ⋆)
    (Ξ» p-holds ⋆ β†’ p-holds)

  anything-implies-itself-is-⊀ : (p : Ξ© 𝓀) β†’ (p β‡’ p) ＝ ⊀
  anything-implies-itself-is-⊀ p =
   Ξ©-extensionality pe fe
    (Ξ» _ β†’ ⋆)
    (Ξ» _ β†’ id)

\end{code}

End of addition.

\section{Disjunction}

\begin{code}

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

 open propositional-truncations-exist pt

 _∨_ : Ξ© 𝓀 β†’ Ξ© π“₯ β†’ Ξ© (𝓀 βŠ” π“₯)
 P ∨ Q = βˆ₯ P holds + Q holds βˆ₯ , βˆ₯βˆ₯-is-prop

 infixr 3 _∨_

\end{code}

Added by Ayberk Tosun 2024-05-28.

\begin{code}

 ∨-elim : (P : Ξ© 𝓀) (Q : Ξ© π“₯) (R : Ξ© 𝓦)
        β†’ (P holds β†’ R holds)
        β†’ (Q holds β†’ R holds)
        β†’ ((P ∨ Q) holds β†’ R holds)
 ∨-elim P Q R Ο† ψ = βˆ₯βˆ₯-rec (holds-is-prop R) †
  where
   † : P holds + Q holds β†’ R holds
   † (inl p) = Ο† p
   † (inr q) = ψ q

\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

 βˆƒβ‚š[κž‰]-syntax : (I : 𝓀 Μ‡ )β†’ (I β†’ Ξ© π“₯)β†’ Ξ© (𝓀 βŠ” π“₯)
 βˆƒβ‚š[κž‰]-syntax I A = Ǝ i κž‰ I , A i holds

 infixr -1 βˆƒ[κž‰]-syntax
 infixr -1 βˆƒ[]-syntax

 syntax βˆƒ[κž‰]-syntax I (Ξ» i β†’ e) = Ǝ i κž‰ I , e
 syntax βˆƒ[]-syntax    (Ξ» i β†’ e) = Ǝ i , e
 syntax βˆƒβ‚š[κž‰]-syntax I (Ξ» i β†’ e) = ΖŽβ‚š i κž‰ 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{Equality}

The following was added by Ayberk Tosun on 2024-05-16.

\begin{code}

module Equality {X : 𝓀 Μ‡ } (s : is-set X) where

 _οΌβ‚š_ : X β†’ X β†’ Ξ© 𝓀
 _οΌβ‚š_ x y = (x ＝ y) , s

 infix 0 _οΌβ‚š_

\end{code}

End of addition.

\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

\end{code}

TODO. Prove the all the missing equations for Heyting algebras for Ξ©.