```\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 3 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 2 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 ()```