--- 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} 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 (π {π€} , π-is-prop) \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} 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 Ξ©.