{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Bool.Properties where

open import Cubical.Core.Everything

open import Cubical.Functions.Involution

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence

open import Cubical.Data.Bool.Base
open import Cubical.Data.Empty

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

notnot : ∀ x → not (not x) ≡ x
notnot true  = refl
notnot false = refl

notIsEquiv : isEquiv not
notIsEquiv = involIsEquiv {f = not} notnot

notEquiv : Bool ≃ Bool
notEquiv = involEquiv {f = not} notnot

notEq : Bool ≡ Bool
notEq = involPath {f = not} notnot

private
variable
ℓ : Level

-- This computes to false as expected
nfalse : Bool
nfalse = transp (λ i → notEq i) i0 true

-- Sanity check
nfalsepath : nfalse ≡ false
nfalsepath = refl

K-Bool
: (P : {b : Bool} → b ≡ b → Type ℓ)
→ (∀{b} → P {b} refl)
→ ∀{b} → (q : b ≡ b) → P q
K-Bool P Pr {false} = J (λ{ false q → P q ; true _ → Lift ⊥ }) Pr
K-Bool P Pr {true}  = J (λ{ true q → P q ; false _ → Lift ⊥ }) Pr

isSetBool : isSet Bool
isSetBool a b = J (λ _ p → ∀ q → p ≡ q) (K-Bool (refl ≡_) refl)

true≢false : ¬ true ≡ false
true≢false p = subst (λ b → if b then Bool else ⊥) p true

false≢true : ¬ false ≡ true
false≢true p = subst (λ b → if b then ⊥ else Bool) p true

not≢const : ∀ x → ¬ not x ≡ x
not≢const false = true≢false
not≢const true  = false≢true

zeroˡ : ∀ x → true or x ≡ true
zeroˡ false = refl
zeroˡ true  = refl

zeroʳ : ∀ x → x or true ≡ true
zeroʳ false = refl
zeroʳ true  = refl

or-identityˡ : ∀ x → false or x ≡ x
or-identityˡ false = refl
or-identityˡ true  = refl

or-identityʳ : ∀ x → x or false ≡ x
or-identityʳ false = refl
or-identityʳ true  = refl

or-comm      : ∀ x y → x or y ≡ y or x
or-comm false y =
false or y ≡⟨ or-identityˡ y ⟩
y          ≡⟨ sym (or-identityʳ y) ⟩
y or false ∎
or-comm true y =
true or y ≡⟨ zeroˡ y ⟩
true      ≡⟨ sym (zeroʳ y) ⟩
y or true ∎

or-assoc     : ∀ x y z → x or (y or z) ≡ (x or y) or z
or-assoc false y z =
false or (y or z)   ≡⟨ or-identityˡ _ ⟩
y or z              ≡[ i ]⟨ or-identityˡ y (~ i) or z ⟩
((false or y) or z) ∎
or-assoc true y z  =
true or (y or z)  ≡⟨ zeroˡ _ ⟩
true             ≡⟨ sym (zeroˡ _) ⟩
true or z        ≡[ i ]⟨ zeroˡ y (~ i) or z ⟩
(true or y) or z ∎

or-idem      : ∀ x → x or x ≡ x
or-idem false = refl
or-idem true  = refl

⊕-identityʳ : ∀ x → x ⊕ false ≡ x
⊕-identityʳ false = refl
⊕-identityʳ true = refl

⊕-comm : ∀ x y → x ⊕ y ≡ y ⊕ x
⊕-comm false false = refl
⊕-comm false true  = refl
⊕-comm true  false = refl
⊕-comm true  true  = refl

⊕-assoc : ∀ x y z → x ⊕ (y ⊕ z) ≡ (x ⊕ y) ⊕ z
⊕-assoc false y z = refl
⊕-assoc true false z = refl
⊕-assoc true true z = notnot z

not-⊕ˡ : ∀ x y → not (x ⊕ y) ≡ not x ⊕ y
not-⊕ˡ false y = refl
not-⊕ˡ true  y = notnot y

⊕-invol : ∀ x y → x ⊕ (x ⊕ y) ≡ y
⊕-invol false x = refl
⊕-invol true  x = notnot x

isEquiv-⊕ : ∀ x → isEquiv (x ⊕_)
isEquiv-⊕ x = involIsEquiv (⊕-invol x)

⊕-Path : ∀ x → Bool ≡ Bool
⊕-Path x = involPath {f = x ⊕_} (⊕-invol x)

⊕-Path-refl : ⊕-Path false ≡ refl
⊕-Path-refl = isInjectiveTransport refl

¬transportNot : ∀(P : Bool ≡ Bool) b → ¬ (transport P (not b) ≡ transport P b)
¬transportNot P b eq = not≢const b sub
where
sub : not b ≡ b
sub = subst {A = Bool → Bool} (λ f → f (not b) ≡ f b)
(λ i c → transport⁻Transport P c i) (cong (transport⁻ P) eq)

module BoolReflection where
data Table (A : Type₀) (P : Bool ≡ A) : Type₀ where
inspect : (b c : A)
→ transport P false ≡ b
→ transport P true ≡ c
→ Table A P

table : ∀ P → Table Bool P
table = J Table (inspect false true refl refl)

reflLemma : (P : Bool ≡ Bool)
→ transport P false ≡ false
→ transport P true ≡ true
→ transport P ≡ transport (⊕-Path false)
reflLemma P ff tt i false = ff i
reflLemma P ff tt i true = tt i

notLemma : (P : Bool ≡ Bool)
→ transport P false ≡ true
→ transport P true ≡ false
→ transport P ≡ transport (⊕-Path true)
notLemma P ft tf i false = ft i
notLemma P ft tf i true  = tf i

categorize : ∀ P → transport P ≡ transport (⊕-Path (transport P false))
categorize P with table P
categorize P | inspect false true p q
= subst (λ b → transport P ≡ transport (⊕-Path b)) (sym p) (reflLemma P p q)
categorize P | inspect true false p q
= subst (λ b → transport P ≡ transport (⊕-Path b)) (sym p) (notLemma P p q)
categorize P | inspect false false p q
= rec (¬transportNot P false (q ∙ sym p))
categorize P | inspect true true p q
= rec (¬transportNot P false (q ∙ sym p))

⊕-complete : ∀ P → P ≡ ⊕-Path (transport P false)
⊕-complete P = isInjectiveTransport (categorize P)

⊕-comp : ∀ p q → ⊕-Path p ∙ ⊕-Path q ≡ ⊕-Path (q ⊕ p)
⊕-comp p q = isInjectiveTransport (λ i x → ⊕-assoc q p x i)

open Iso

reflectIso : Iso Bool (Bool ≡ Bool)
reflectIso .fun = ⊕-Path
reflectIso .inv P = transport P false
reflectIso .leftInv = ⊕-identityʳ
reflectIso .rightInv P = sym (⊕-complete P)

reflectEquiv : Bool ≃ (Bool ≡ Bool)
reflectEquiv = isoToEquiv reflectIso