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 4 _â§_ \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 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 _â_ \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 3 _â¨_ \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 40 _ââ_ _ââ_ : {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}