Logic
--- title: Logic author: Martín Escardó and Ayberk Tosun date-started: 2021-03-10 --- Based in part by the `Cubical.Functions.Logic` module of `agda/cubical`.{-# 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\section{Negation}module Negation (fe : funext 𝓤 𝓤₀) where ⇁_ : Ω 𝓤 → Ω 𝓤 ⇁_ = not fe ⇁⇁_ : Ω 𝓤 → Ω 𝓤 ⇁⇁ p = ⇁(⇁ p)\section{Conjunction}module Conjunction where _∧_ : Ω 𝓤 → Ω 𝓥 → Ω (𝓤 ⊔ 𝓥) P ∧ Q = (P holds × Q holds) , γ where γ = ×-is-prop (holds-is-prop P) (holds-is-prop Q) infixr 4 _∧_Added by Martin Escardo 1st Nov 2023.∧-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))Added by Martin Escardo 8th September 2025.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)TODO. Add all the semilattice equations. End of addition. \section{Universal quantification}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\section{Implication}module Implication (fe : Fun-Ext) where 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)Added by Martin Escardo 1st Nov 2023.⇔-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 _ _))Added by Martin Escardo 8th September 2025.⊥⇒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 of addition. \section{Disjunction}module Disjunction (pt : propositional-truncations-exist) where open propositional-truncations-exist pt _∨_ : Ω 𝓤 → Ω 𝓥 → Ω (𝓤 ⊔ 𝓥) P ∨ Q = ∥ P holds + Q holds ∥ , ∥∥-is-prop infixr 3 _∨_Added by Ayberk Tosun 2024-05-28.∨-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\section{Truncation}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)\section{Existential quantification}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\section{Negation of equality}module Negation-of-equality (fe : Fun-Ext) where _≢_ : {X : 𝓤 ̇ } → X → X → Ω 𝓤 x ≢ y = (x ≠ y) , Π-is-prop fe (λ _ → 𝟘-is-prop)\section{Equality} The following was added by Ayberk Tosun on 2024-05-16.module Equality {X : 𝓤 ̇ } (s : is-set X) where _＝ₚ_ : X → X → Ω 𝓤 _＝ₚ_ x y = (x ＝ y) , s infix 0 _＝ₚ_End of addition. \section{A module for importing all combinators}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 publicTODO. Prove the all the missing equations for Heyting algebras for Ω.