\import Logic
\import Meta
\import Paths

\data Bool | false | true

\func So (b : Bool) : \Prop
  | true => \Sigma
  | false => Empty
  \where {
    \lemma fromSo {b : Bool} (s : So b) : b = true \elim b
      | true => idp

    \lemma toSo {b : Bool} (p : b = true) : So b
      => transportInv So p ()
  }

\func not (b : Bool) : Bool
  | true => false
  | false => true

\lemma not-isInv {b : Bool} : not (not b) = b
  => cases b idp

\func if {A : \Type} (b : Bool) (then else : A) : A \elim b
  | true => then
  | false => else

\func \infixl  and (x y : Bool) : Bool \elim x
  | true => y
  | false => false
  \where {
    \lemma toSigma {x y : Bool} (p : x and y = true) : \Sigma (x = true) (y = true) \elim x, y, p
      | true, true, _ => (idp,idp)

    \lemma fromSigma {x y : Bool} (p : \Sigma (x = true) (y = true)) : x and y = true \elim x, y, p
      | true, true, _ => idp
      | false, _, ((),_)
      | _, false, (_,())
  }

\func \infixl  or (x y : Bool) : Bool \elim x
  | true => true
  | false => y
  \where {
    \lemma toOr {x y : Bool} (p : x or y = true) : (x = true) || (y = true) \elim x, y, p
      | true, _, _ => byLeft idp
      | _, true, _ => byRight idp

    \lemma fromOr {x y : Bool} (p : (x = true) || (y = true)) : x or y = true \elim x, y, p
      | true, _, _ => idp
      | false, true, _ => idp
      | false, false, byLeft ()
      | false, false, byRight ()
  }

\lemma true/=false (p : true = false) : Empty => transport So p ()