\begin{code}

{-# OPTIONS --safe --without-K #-}

module MLTT.Bool where

open import MLTT.Spartan

data Bool : ๐“คโ‚€ ฬ‡ where
 true false : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN FALSE false #-}
{-# BUILTIN TRUE  true  #-}

true-is-not-false : true โ‰  false
true-is-not-false p = transport f p โ‹†
 where
  f : Bool โ†’ ๐“คโ‚€ ฬ‡
  f true  = ๐Ÿ™
  f false = ๐Ÿ˜

if_then_else_ : {X : ๐“ค ฬ‡ } โ†’ Bool โ†’ X โ†’ X โ†’ X
if true  then x else y = x
if false then x else y = y

Bool-induction : (A : Bool โ†’ ๐“ค ฬ‡ ) โ†’ A true โ†’ A false โ†’ (b : Bool) โ†’ A b
Bool-induction A x y true  = x
Bool-induction A x y false = y

Bool-equality-cases : {A : ๐“ค ฬ‡ } (x : Bool)
                    โ†’ (x ๏ผ true โ†’ A) โ†’ (x ๏ผ false โ†’ A) โ†’ A
Bool-equality-cases true  f g = f refl
Bool-equality-cases false f g = g refl

not : Bool โ†’ Bool
not false = true
not true  = false

_||_ _&&_ : Bool โ†’ Bool โ†’ Bool

true  || y = true
false || y = y

true  && y = y
false && y = false

true-right-||-absorptive : (x : Bool) โ†’ x || true ๏ผ true
true-right-||-absorptive true  = refl
true-right-||-absorptive false = refl

||-left-intro : ({x} y : Bool) โ†’ x ๏ผ true โ†’ x || y ๏ผ true
||-left-intro {true}  y e = refl
||-left-intro {false} y e = ๐Ÿ˜-elim (true-is-not-false (e โปยน))

||-right-intro : ({x} y : Bool) โ†’ y ๏ผ true โ†’ x || y ๏ผ true
||-right-intro {true}  true  e = refl
||-right-intro {true}  false e = refl
||-right-intro {false} true  e = refl
||-right-intro {false} false e = e

||-gives-+ : {x y : Bool} โ†’ x || y ๏ผ true โ†’ (x ๏ผ true) + (y ๏ผ true)
||-gives-+ {true}  {y}     e = inl refl
||-gives-+ {false} {true}  e = inr refl
||-gives-+ {false} {false} e = inl e

&&-gives-ร— : {x y : Bool} โ†’ x && y ๏ผ true โ†’ (x ๏ผ true) ร— (y ๏ผ true)
&&-gives-ร— {true}  {true}  e = refl , refl
&&-gives-ร— {true}  {false} e = refl , e
&&-gives-ร— {false} {y}     e = ๐Ÿ˜-elim (true-is-not-false (e โปยน))

&&-intro : {x y : Bool} โ†’ x ๏ผ true โ†’ y ๏ผ true โ†’ x && y ๏ผ true
&&-intro {true}  {true}  p q = refl
&&-intro {true}  {false} p q = q
&&-intro {false} {y}     p q = p

infixl 10 _||_
infixl 20 _&&_

record Eq {๐“ค} (X : ๐“ค ฬ‡ ) : ๐“ค ฬ‡ where
  field
    _==_    : X โ†’ X โ†’ Bool
    ==-refl : (x : X) โ†’ (x == x) ๏ผ true

open Eq {{...}} public

โ„•-== : โ„• โ†’ โ„• โ†’ Bool
โ„•-== 0        0        = true
โ„•-== 0        (succ y) = false
โ„•-== (succ x) 0        = false
โ„•-== (succ x) (succ y) = โ„•-== x y

โ„•-refl : (n : โ„•) โ†’ (โ„•-== n n) ๏ผ true
โ„•-refl 0        = refl
โ„•-refl (succ n) = โ„•-refl n

instance
 eqโ„• : Eq โ„•
 _==_    {{eqโ„•}} = โ„•-==
 ==-refl {{eqโ„•}} = โ„•-refl

\end{code}