\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}