\begin{code} {-# OPTIONS --safe #-} module Truth where open import Prelude hiding (⊤; tt) renaming (Poly-⊤ to ⊤; Poly-tt to tt) private module DisplayOmega where \end{code} %<*omega> \begin{code}[number=truth-def] record Ω : Type₁ where field ProofOf : Type IsProp : isProp ProofOf \end{code} %</omega> \begin{code} open Ω \end{code} %<*true> \begin{code} True : Ω ProofOf True = ⊤ IsProp True _ _ = refl \end{code} %</true> %<*false> \begin{code} False : Ω ProofOf False = ⊥ IsProp False () \end{code} %</false> \begin{code} open import Data.Nat.Properties using (isSetNat; _mod_) \end{code} %<*true-false> \begin{code}[number=three-is-even] 3-is-even : Ω ProofOf 3-is-even = 3 mod 2 ≡ 0 IsProp 3-is-even = isSetNat _ _ \end{code} %</true-false> \begin{code} module _ {A : Type} where \end{code} %<*equality> \begin{code} _|≡|_ : A → A → Ω ProofOf (x |≡| y) = ∥ x ≡ y ∥ IsProp (x |≡| y) = squash \end{code} %</equality> \begin{code} infix 3 _∥_ record Ω p : Type (ℓsuc p) where constructor _∥_; no-eta-equality field ProofOf : Type p IsProp : isProp ProofOf open Ω public True : Ω a ProofOf True = ⊤ IsProp True _ _ = refl open import Cubical.Foundations.HLevels using (isPropIsOfHLevel) cong-∥ : (x y : Ω a) → (lhs : ProofOf x ≡ ProofOf y) → PathP (λ i → isProp (lhs i)) (IsProp x) (IsProp y) → x ≡ y cong-∥ x y lhs rhs i .ProofOf = lhs i cong-∥ x y lhs rhs i .IsProp = rhs i Ω≡ : (x y : Ω a) → ProofOf x ≡ ProofOf y → x ≡ y Ω≡ x y p = cong-∥ x y p (J (λ y idxy → ∀ lhs rhs → PathP (λ i → isProp (idxy i)) lhs rhs) (isPropIsOfHLevel 1) p (IsProp x) (IsProp y)) private variable X Y Z : Ω a \end{code} %<*iff> \begin{code} _iff_ : (ProofOf X → ProofOf Y) → (ProofOf Y → ProofOf X) → X ≡ Y \end{code} %</iff> \begin{code} _iff_ {X = x} {Y = y} lhs rhs = Ω≡ x y (isoToPath (iso lhs rhs (λ _ → y .IsProp _ _) λ _ → x .IsProp _ _)) proves-lhs : (x : Ω a) → ProofOf x → ProofOf x ≡ ⊤ proves-lhs x p = isoToPath (iso (const tt) (const p) (λ _ → refl) λ _ → IsProp x _ _) proves : ProofOf X → X ≡ True proves p = const tt iff const p module LevelZero where False : Ω _ ProofOf False = ⊥ IsProp False () disproves : (ProofOf X → ⊥) → X ≡ False disproves ¬p = ¬p iff absurd open import Data.Nat.Properties using (isSetNat; _mod_; suc≢zero) \end{code} %<*one-neq-zero> \begin{code}[inline] 1≢0 : 1 ≡ 0 → ⊥ \end{code} %</one-neq-zero> \begin{code} 1≢0 = suc≢zero 3-is-even : Ω 0 ProofOf 3-is-even = 3 mod 2 ≡ 0 IsProp 3-is-even = isSetNat _ _ \end{code} %<*3-is-not-even> \begin{code} 3-is-not-even : 3-is-even ≡ False 3-is-not-even = 1≢0 iff absurd \end{code} %</3-is-not-even> \begin{code} module _ {a : Level} where False : Ω a False .ProofOf = Poly-⊥ False .IsProp () disproves : (ProofOf X → ⊥) → X ≡ False disproves p = (absurd ∘ p) iff λ () at-most-two : ∄ p × p ≢ True × p ≢ False at-most-two (p , p≢True , p≢False) = p≢False (disproves (p≢True ∘ proves)) Decided : ∀ ℓ → Type (ℓsuc ℓ) Decided ℓ = Σ[ P ⦂ Ω ℓ ] × Dec (P .ProofOf) module IsoDec {a : Level} where inv-fnc : Bool → Decided a inv-fnc = bool (False , no λ ()) (True , yes _) left-inv : (x : Decided a) → inv-fnc (does (x .snd)) .fst ≡ x .fst left-inv (P , yes p) = sym (proves p) left-inv (P , no ¬p) = sym (disproves ¬p) DecΩ⇔Bool : Decided a ⇔ Bool DecΩ⇔Bool .fun (_ , x) = does x DecΩ⇔Bool .inv = inv-fnc DecΩ⇔Bool .rightInv false = refl DecΩ⇔Bool .rightInv true = refl DecΩ⇔Bool .leftInv x = Σ≡Prop (λ p → isPropDec (p .IsProp)) (left-inv x) DecΩ≡Bool : Decided a ≡ Lift Bool DecΩ≡Bool = isoToPath (DecΩ⇔Bool ⟨ trans-⇔ ⟩ lift⇔) open IsoDec public using (DecΩ⇔Bool; DecΩ≡Bool) extract : {x : Ω a} → x ≡ True → ProofOf x extract p = subst ProofOf (sym p) tt open import Cubical.Foundations.HLevels Truth⇔hProp : Ω a ⇔ hProp a Truth⇔hProp .fun x .fst = x .ProofOf Truth⇔hProp .fun x .snd = x .IsProp Truth⇔hProp .inv x .ProofOf = x .fst Truth⇔hProp .inv x .IsProp = x .snd Truth⇔hProp .rightInv b = refl Truth⇔hProp .leftInv x i .ProofOf = x .ProofOf Truth⇔hProp .leftInv x i .IsProp = x .IsProp abstract isSetΩ : isSet (Ω a) isSetΩ = subst isSet (sym (isoToPath Truth⇔hProp)) isSetHProp open import Cubical.HITs.PropositionalTruncation interleaved mutual infixl 7 _|∧|_ _|∧|_ : Ω a → Ω a → Ω _ infixl 6 _|∨|_ _|∨|_ : Ω a → Ω b → Ω _ infixr 5 _|→|_ _|→|_ : Ω a → Ω b → Ω _ \end{code} %<*logic> \begin{code} ProofOf (X |∧| Y) = ProofOf X × ProofOf Y ProofOf (X |→| Y) = ProofOf X → ProofOf Y ProofOf (X |∨| Y) = ∥ ProofOf X ⊎ ProofOf Y ∥ \end{code} %</logic> \begin{code} IsProp (_ |→| Y) = isProp→ (IsProp Y) IsProp (x |∧| y) = isProp× (x .IsProp) (y .IsProp) IsProp (x |∨| y) = squash |∀| : (A → Ω b) → Ω _ ProofOf (|∀| f) = ∀ x → ProofOf (f x) IsProp (|∀| f) = isPropΠ λ x → IsProp (f x) |∃| : (A → Ω b) → Ω _ ProofOf (|∃| f) = ∥ ∃ x × ProofOf (f x) ∥ IsProp (|∃| f) = squash _|↔|_ : Ω a → Ω b → Ω _ X |↔| Y = (X |→| Y) |∧| (Y |→| X) |→|-id : (x : Ω a) → x |→| x ≡ True |→|-id x = proves id Not : Ω a → Ω a Not x .ProofOf = ¬ x .ProofOf Not x .IsProp = isProp→ λ () |→|-idˡ : (x : Ω a) → True |→| x ≡ x |→|-idˡ {a = a} x = (_$ (tt {ℓ = a})) iff const |→|-annʳ : (x : Ω a) → x |→| True {a = b} ≡ True |→|-annʳ x = const tt iff (λ _ _ → tt) |→|-annˡ : (x : Ω a) → False {a = b} |→| x ≡ True |→|-annˡ x = (λ _ → tt) iff λ _ () Ω∣_∣ : Type a → Ω a ProofOf Ω∣ P ∣ = ∥ P ∥ IsProp Ω∣ P ∣ = squash infix 5.5 _|≡|_ _|≡|_ : A → A → Ω _ x |≡| y = Ω∣ x ≡ y ∣ |T| : Bool → Ω a |T| = bool′ False True |→|-trans : (x y z : Ω a) → ((x |→| y) |∧| (y |→| z)) |→| (x |→| z) ≡ True |→|-trans x y z = const tt iff const (uncurry (flip _∘_)) |→|-curry : (X Y Z : Ω a) → (X |∧| Y |→| Z) ≡ (X |→| Y |→| Z) |→|-curry _ _ _ = curry iff uncurry |→|-|∧| : (x y z : Ω a) → (x |→| (y |∧| z)) ≡ (x |→| y) |∧| (x |→| z) |→|-|∧| _ _ _ = (λ f → fst ∘ f , snd ∘ f) iff λ { (f , g) x → f x , g x } |∨|-|→| : (x y z : Ω a) → ((x |∨| y) |→| z) ≡ (x |→| z) |∧| (y |→| z) |∨|-|→| _ _ z = (λ f → f ∘ ∣_∣ ∘ inl , f ∘ ∣_∣ ∘ inr) iff λ { (f , g) → rec (z .IsProp) (either f g) } ∧-com : (x y : Ω a) → x |∧| y ≡ y |∧| x ∧-com _ _ = (λ { (x , y) → (y , x) }) iff λ { (x , y) → y , x } ∧-idem : (x : Ω a) → x |∧| x ≡ x ∧-idem _ = fst iff (λ x → x , x) ∨-idem : (x : Ω a) → x |∨| x ≡ x ∨-idem x = (rec (x .IsProp) (either id id)) iff (∣_∣ ∘ inl) ∨-com : (x y : Ω a) → x |∨| y ≡ y |∨| x ∨-com x y = (rec squash (∣_∣ ∘ either inr inl)) iff (rec squash (∣_∣ ∘ either inr inl)) ∧-ann : (x : Ω a) → x |∧| (False {a}) ≡ False ∧-ann x = snd iff λ () refute : (x : Ω a) → ¬ ProofOf x → x ≡ False refute x ¬p = (absurd ∘ ¬p) iff λ () ∨-assoc : (x y z : Ω a) → (x |∨| y) |∨| z ≡ x |∨| (y |∨| z) ∨-assoc x y z = (rec squash (either (rec squash (∣_∣ ∘ mapʳ (∣_∣ ∘ inl))) (∣_∣ ∘ inr ∘ ∣_∣ ∘ inr ))) iff (rec squash (either (∣_∣ ∘ inl ∘ ∣_∣ ∘ inl) (rec squash (∣_∣ ∘ mapˡ (∣_∣ ∘ inr) )))) ∧-assoc : (x y z : Ω a) → (x |∧| y) |∧| z ≡ x |∧| (y |∧| z) ∧-assoc x y z = (λ { ((x , y) , z) → x , y , z }) iff λ { (x , y , z) → (x , y) , z } ∧-id : (x : Ω a) → (True {a}) |∧| x ≡ x ∧-id x = snd iff (tt ,_) ∨-ann : (x : Ω a) → x |∨| (True {a}) ≡ True ∨-ann x = (const tt) iff (∣_∣ ∘ inr) ∨-id : (x : Ω a) → x |∨| (False {a}) ≡ x ∨-id x = (rec (x .IsProp) (either id (λ ()))) iff (∣_∣ ∘ inl) ∨-idˡ : (x : Ω a) → (False {a}) |∨| x ≡ x ∨-idˡ x = (rec (x .IsProp) (either (λ ()) id)) iff (∣_∣ ∘ inr) ∧-distrib-∨ : (x y z : Ω a) → x |∧| (y |∨| z) ≡ (x |∧| y) |∨| (x |∧| z) ∧-distrib-∨ x y z = (uncurry (λ xp → rec squash (∣_∣ ∘ map-⊎ (xp ,_) (xp ,_)) )) iff (rec (isProp× (x .IsProp) squash) (either (map₂ (∣_∣ ∘ inl)) (map₂ (∣_∣ ∘ inr)))) ∨-distrib-∧ : (x y z : Ω a) → x |∨| (y |∧| z) ≡ (x |∨| y) |∧| (x |∨| z) ∨-distrib-∧ x y z = (rec (isProp× squash squash) (either (λ x → ∣ inl x ∣ , ∣ inl x ∣) λ { (yp , zp) → ∣ inr yp ∣ , ∣ inr zp ∣ })) iff (uncurry (rec2 squash λ { (inl x) _ → ∣ inl x ∣ ; _ (inl x) → ∣ inl x ∣ ; (inr y) (inr z) → ∣ inr (y , z) ∣ })) \end{code}