open import 1Lab.Path.IdentitySystem
open import 1Lab.HLevel.Retracts
open import 1Lab.Univalence
open import 1Lab.Type.Dec
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open is-equiv
open is-contr
open is-iso

module Data.Bool where

open import 1Lab.Prim.Data.Bool public

The BooleansπŸ”—

The type of booleans is interesting in homotopy type theory because it is the simplest type where its automorphisms in Type are non-trivial. In particular, there are two: negation, and the identity.

But first, true isn’t false.

trueβ‰ false : true ≑ false β†’ βŠ₯
true≠false p = subst P p tt where
  P : Bool β†’ Type
  P false = βŠ₯
  P true = ⊀

It’s worth noting how to prove two things are not equal. We write a predicate that distinguishes them by mapping one to ⊀, and one to βŠ₯. Then we can substitute under P along the claimed equality to get an element of βŠ₯ - a contradiction.

Basic algebraic propertiesπŸ”—

The booleans form a Boolean algebra, as one might already expect, given its name. The operations required to define such a structure are straightforward to define using pattern matching:

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

Pattern matching on only the first argument might seem like a somewhat inpractical choice due to its asymmetry - however, it shortens a lot of proofs since we get a lot of judgemental equalities for free. For example, see the following statements:

and-associative : (x y z : Bool) β†’ and x (and y z) ≑ and (and x y) z
and-associative false y z = refl
and-associative true y z = refl

or-associative : (x y z : Bool) β†’ or x (or y z) ≑ or (or x y) z
or-associative false y z = refl
or-associative true y z = refl

and-commutative : (x y : Bool) β†’ and x y ≑ and y x
and-commutative false false = refl
and-commutative false true = refl
and-commutative true false = refl
and-commutative true true = refl

or-commutative : (x y : Bool) β†’ or x y ≑ or y x
or-commutative false false = refl
or-commutative false true = refl
or-commutative true false = refl
or-commutative true true = refl

and-truer : (x : Bool) β†’ and x true ≑ x
and-truer false = refl
and-truer true = refl

and-falser : (x : Bool) β†’ and x false ≑ false
and-falser false = refl
and-falser true = refl

and-truel : (x : Bool) β†’ and true x ≑ x
and-truel x = refl

or-falser : (x : Bool) β†’ or x false ≑ x
or-falser false = refl
or-falser true = refl

or-truer : (x : Bool) β†’ or x true ≑ true
or-truer false = refl
or-truer true = refl

or-falsel : (x : Bool) β†’ or false x ≑ x
or-falsel x = refl

and-absorbs-orr : (x y : Bool) β†’ and x (or x y) ≑ x
and-absorbs-orr false y = refl
and-absorbs-orr true y = refl

or-absorbs-andr : (x y : Bool) β†’ or x (and x y) ≑ x
or-absorbs-andr false y = refl
or-absorbs-andr true y = refl

and-distrib-orl : (x y z : Bool) β†’ and x (or y z) ≑ or (and x y) (and x z)
and-distrib-orl false y z = refl
and-distrib-orl true y z = refl

or-distrib-andl : (x y z : Bool) β†’ or x (and y z) ≑ and (or x y) (or x z)
or-distrib-andl false y z = refl
or-distrib-andl true y z = refl

and-idempotent : (x : Bool) β†’ and x x ≑ x
and-idempotent false = refl
and-idempotent true = refl

or-idempotent : (x : Bool) β†’ or x x ≑ x
or-idempotent false = refl
or-idempotent true = refl

All the properties above hold both in classical and constructive mathematics, even in minimal logic that fails to validate both the law of the excluded middle as well as the law of noncontradiction. However, the boolean operations satisfy both of these laws:

not-involutive : (x : Bool) β†’ not (not x) ≑ x
not-involutive false i = false
not-involutive true i = true

not-and≑or-not : (x y : Bool) β†’ not (and x y) ≑ or (not x) (not y)
not-and≑or-not false y = refl
not-and≑or-not true y = refl

not-or≑and-not : (x y : Bool) β†’ not (or x y) ≑ and (not x) (not y)
not-or≑and-not false y = refl
not-or≑and-not true y = refl

or-complementl : (x : Bool) β†’ or (not x) x ≑ true
or-complementl false = refl
or-complementl true = refl

and-complementl : (x : Bool) β†’ and (not x) x ≑ false
and-complementl false = refl
and-complementl true = refl

Exclusive disjunction (usually known as XOR) also yields additional structure - in particular, it can be viewed as an addition operator in a ring whose multiplication is defined by conjunction:

xor : Bool β†’ Bool β†’ Bool
xor false y = y
xor true y = not y

xor-associative : (x y z : Bool) β†’ xor x (xor y z) ≑ xor (xor x y) z
xor-associative false y z = refl
xor-associative true false z = refl
xor-associative true true z = not-involutive z

xor-commutative : (x y : Bool) β†’ xor x y ≑ xor y x
xor-commutative false false = refl
xor-commutative false true = refl
xor-commutative true false = refl
xor-commutative true true = refl

xor-falser : (x : Bool) β†’ xor x false ≑ x
xor-falser false = refl
xor-falser true = refl

xor-truer : (x : Bool) β†’ xor x true ≑ not x
xor-truer false = refl
xor-truer true = refl

xor-inverse-self : (x : Bool) β†’ xor x x ≑ false
xor-inverse-self false = refl
xor-inverse-self true = refl

and-distrib-xorr : (x y z : Bool) β†’ and (xor x y) z ≑ xor (and x z) (and y z)
and-distrib-xorr false y z = refl
and-distrib-xorr true y false = and-falser (not y) βˆ™ sym (and-falser y)
and-distrib-xorr true y true = (and-truer (not y)) βˆ™ ap not (sym (and-truer y))

Material implication between booleans also interacts nicely with many of the other operations:

imp : Bool β†’ Bool β†’ Bool
imp false y = true
imp true y = y

imp-truer : (x : Bool) β†’ imp x true ≑ true
imp-truer false = refl
imp-truer true = refl

DiscretenessπŸ”—

Using pattern matching, and the fact that true isn't false, one can write an algorithm to tell whether or not two booleans are the same:

Discrete-Bool : Discrete Bool
Discrete-Bool false false = yes refl
Discrete-Bool false true = no (λ p → true≠false (sym p))
Discrete-Bool true false = no true≠false
Discrete-Bool true true = yes refl

Bool-is-set : is-set Bool
Bool-is-set = Discrete→is-set Discrete-Bool

instance
  H-Level-Bool : βˆ€ {n} β†’ H-Level Bool (2 + n)
  H-Level-Bool = basic-instance 2 Bool-is-set

Furthermore, if we know we’re not looking at true, then we must be looking at false, and vice-versa:

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

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-is-equiv : is-equiv not
not-is-equiv = is-iso→is-equiv (iso not not-involutive not-involutive)

Aut(Bool)πŸ”—

We characterise the type Bool ≑ Bool. There are exactly two paths, and we can decide which path we’re looking at by seeing how it acts on the element true.

First, two small lemmas: we can tell whether we’re looking at the identity equivalence or the β€œnot” equivalence by seeing how it acts on the constructors.

private
  idLemma : (p : Bool ≃ Bool)
          β†’ p .fst true ≑ true
          β†’ p .fst false ≑ false
          β†’ p ≑ (_ , id-equiv)
  idLemma p p1 p2 = Ξ£-path (funext lemma) (is-equiv-is-prop _ _ _) where
    lemma : (x : Bool) β†’ _
    lemma false = p2
    lemma true = p1

If it quacks like the identity equivalence, then it must be. Otherwise we’re looking at the not equivalence.

  notLemma : (p : Bool ≃ Bool)
           β†’ p .fst true ≑ false
           β†’ p .fst false ≑ true
           β†’ p ≑ (not , not-is-equiv)
  notLemma p p1 p2 = Ξ£-path (funext lemma) (is-equiv-is-prop _ _ _) where
    lemma : (x : Bool) β†’ _
    lemma false = p2
    lemma true = p1

With these two lemmas, we can proceed to classify the automorphisms of Bool. For this, we’ll need another lemma: If a function Bool β†’ Bool doesn’t map f x ≑ x, then it maps f x ≑ not x.

Bool-aut≑2 : (Bool ≑ Bool) ≑ Lift _ Bool
Bool-aut≑2 = Isoβ†’Path the-iso where
  lemma : (f : Bool β†’ Bool) {x : Bool} β†’ (f x ≑ x β†’ βŠ₯) β†’ f x ≑ not x
  lemma f {false} x with Discrete-Bool (f false) true
  lemma f {false} x | yes p = p
  lemma f {false} x | no Β¬p = absurd (Β¬p (xβ‰ falseβ†’x≑true _ x))

  lemma f {true} x with Discrete-Bool (f true) false
  lemma f {true} x | yes p = p
  lemma f {true} x | no Β¬p = absurd (Β¬p (xβ‰ trueβ†’x≑false _ x))

This lemma is slightly annoying to prove, but it’s not too complicated. It’s essentially two case splits: first on the boolean, and second on whether we’re looking at f x ≑ not x. If we are, then it’s fine (those are the yes p = p cases) - otherwise that contradicts what we’ve been told.

  the-iso : Iso (Bool ≑ Bool) (Lift _ Bool)

  fst the-iso path with Discrete-Bool (transport path true) true
  ... | yes path = lift false
  ... | no Β¬path = lift true

Now we classify the isomorphism by looking at what it does to true. We arbitrarily map refl to false and not to true.

  the-iso .snd .is-iso.inv (lift false) = refl
  the-iso .snd .is-iso.inv (lift true)  = ua (not , not-is-equiv)

The inverse is determined by the same rule, but backwards. That’s why it’s an inverse! Everything computes in a way that lines up to this function being a right inverse on the nose.

  the-iso .snd .is-iso.rinv (lift false) = refl
  the-iso .snd .is-iso.rinv (lift true) = refl

The left inverse is a lot more complicated to prove. We examine how the path acts on both true and false. There are four cases:

  the-iso .snd .is-iso.linv path with Discrete-Bool (transport path true) true
                                     | Discrete-Bool (transport path false) false
  ... | yes true→true | yes false→false =
    refl                  β‰‘βŸ¨ sym (Path≃Equiv .snd .linv _) βŸ©β‰‘
    ua (pathβ†’equiv refl) β‰‘βŸ¨ ap ua pathβ†’equiv-refl βŸ©β‰‘
    ua (_ , id-equiv)      β‰‘βŸ¨ ap ua (sym (idLemma _ trueβ†’true falseβ†’false)) βŸ©β‰‘
    ua (pathβ†’equiv path) β‰‘βŸ¨ Path≃Equiv .snd .linv _ βŸ©β‰‘
    path                  ∎

In the case where the path quacks like reflexivity, we use the univalence axiom to show that we must be looking at the reflexivity path. For this, we use idLemma to show that path→equiv path must be the identity equivalence.

  ... | yes true→true | no false→true' =
    let
      false→true = lemma (transport path) false→true'
      fibres = is-contr→is-prop (path→equiv path .snd .is-eqv true)
                              (true , true→true) (false , false→true)
    in absurd (true≠false (ap fst fibres))

The second case is when both booleans map to true. This is a contradiction - transport along a path is an equivalence, and equivalences have contractible fibres; Since we have two fibres over true, that means we must have true ≑ false.

  ... | no true→false' | yes false→false =
    let
      true→false = lemma (transport path) true→false'
      fibres = is-contr→is-prop (path→equiv path .snd .is-eqv false)
                              (true , true→false) (false , false→false)
    in absurd (true≠false (ap fst fibres))

The other case is analogous.

  ... | no true→false' | no false→true' =
    ua (not , not-is-equiv) β‰‘βŸ¨ ap ua (sym (notLemma _
                                            (lemma (transport path) true→false')
                                            (lemma (transport path) false→true')))
                            βŸ©β‰‘
    ua (pathβ†’equiv path)  β‰‘βŸ¨ Path≃Equiv .snd .linv _ βŸ©β‰‘
    path                   ∎

The last case is when the path quacks like ua (not, _) - in that case, we use the notLemma to show it must be ua (not, _), and the univalence axiom finishes the job.