open import 1Lab.Path.IdentitySystem
open import 1Lab.HLevel.Closure
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.Dec.Base

module Data.Bool.Base where

open import Prim.Data.Bool public

true≠false : ¬ true ≡ false
true≠false p = subst P p tt where
  P : Bool → Type
  P false = ⊥
  P true = ⊤

false≠true : ¬ false ≡ true
false≠true = true≠false ∘ sym

not : Bool → Bool
not true = false
not false = true

and or : Bool → Bool → Bool
and false y = false
and true y = y

or false y = y
or true y = true

instance
  Discrete-Bool : Discrete Bool
  Discrete-Bool .decide false false = yes refl
  Discrete-Bool .decide false true  = no false≠true
  Discrete-Bool .decide true  false = no true≠false
  Discrete-Bool .decide true  true  = yes refl

instance
  H-Level-Bool : ∀ {n} → H-Level Bool (2 + n)
  H-Level-Bool = basic-instance 2 (Discrete→is-set auto)

x≠true→x≡false : (x : Bool) → x ≠ true → x ≡ false
x≠true→x≡false false p = refl
x≠true→x≡false true p = absurd (p refl)

x≠false→x≡true : (x : Bool) → x ≠ false → x ≡ true
x≠false→x≡true false p = absurd (p refl)
x≠false→x≡true true p = refl

if : ∀ {ℓ} {A : Type ℓ} → A → A → Bool → A
if x y false = y
if x y true = x

infix 0 if_then_else_

if_then_else_ : ∀ {ℓ} {A : Type ℓ} → Bool → A → A → A
if false then t else f = f
if true then t else f = t

Bool-elim : ∀ {ℓ} (A : Bool → Type ℓ) → A true → A false → ∀ x → A x
Bool-elim A at af true = at
Bool-elim A at af false = af

record So (b : Bool) : Type where
  constructor oh
  field
    ⦃ is-so ⦄ : if b then ⊤ˢ else ⊥ˢ

¬so-false : So false → ⊥
¬so-false ()

oh? : ∀ x → Dec (So x)
oh? true = yes oh
oh? false = no λ ()

not-so : ∀ {x} → ¬ So x → So (not x)
not-so {true} ¬p = absurd (¬p oh)
not-so {false} ¬p = oh

instance
  H-Level-So : ∀ {x n} → H-Level (So x) (suc n)
  H-Level-So = prop-instance (λ _ _ → refl)

  Dec-So : ∀ {x} → Dec (So x)
  Dec-So {x} = oh? x

The “not” equivalence🔗

The construction of not as an equivalence factors through showing that not is an isomorphism. In particular, not is its own inverse, so we need a proof that it’s involutive, as is proven in not-involutive. With this, we can get a proof that it’s an equivalence:

not-involutive : (x : Bool) → not (not x) ≡ x
not-involutive false i = false
not-involutive true  i = true

not-is-equiv : is-equiv not
not-is-equiv = is-involutive→is-equiv not-involutive

not≃ : Bool ≃ Bool
not≃ = not , not-is-equiv