UniAgda.Equiv.Bool

Table of Contents

1 Prelude

2 Bool is equivalent to (equiv Bool Bool)

We first need to define functions each way.

private
  f : Bool  Bool  Bool
  f (h , X) = h true

  g : Bool  Bool  Bool
  g true = equiv-adjointify (id , id , hrefl , hrefl)
  g false = equiv-adjointify (swap , swap ,
                                    { true  refl
                                      ; false  refl}) ,
                                   λ { true  refl
                                     ; false  refl})

Now we need the required homotopies. The first is easy.

private
  η : f o g ~ id
  η true = refl
  η false = refl

For the second, we need the to use three important results regarding Bool. The first is that every \(x\) in Bool is equal to true or false.

eq-T-F-Bool : (x : Bool)  (x  true) + (x  false)
eq-T-F-Bool true = inl refl 
eq-T-F-Bool false = inr refl 

Next, we show that true cannot equal false.

true-neq-false : ¬ (true  false)
true-neq-false p = transport  { true  Unit ; false  Empty}) p tt

Finally, we need that every equivalence on Bool commutes with \(\text{swap}\). That is, if \(f: \text{Bool} \to \text{Bool}\) is an equivalence, then \(\text{swap} \circ f = f \circ \text{swap}\). This is just done by a case analysis on both \(h(true), h(false)\) being true or false.

Bool-autoequiv-not-const : (H : Bool  Bool)  (pr₁ H o swap ~ swap o pr₁ H)
Bool-autoequiv-not-const (h , h' , α , β , γ) with (eq-T-F-Bool (h true)) | eq-T-F-Bool (h false)
... | inl q | inl s = λ {x  Empty-ind (true-neq-false (α true ^  ap h' (q  s ^)  α false))}
... | inl q | inr s = λ { true  s  ap swap q ^
                        ; false  q  ap swap s ^}
... | inr q | inl s = λ { true  s  ap swap q ^
                        ; false  q  ap swap s ^}
... | inr q | inr s = λ {x  Empty-ind (true-neq-false (α true ^  ap h' (q  s ^)  α false))}

We are now ready to give the final homotopy.

private
  ϵ : g o f ~ id
  ϵ (h , h' , α , β , γ) with eq-T-F-Bool (h true) | eq-T-F-Bool (h false)
  ... | inl q | inl s = fibres-props-eq
                        isEquiv-is-prop _ _
                        (funext λ { x  Empty-ind $ true-neq-false
                          (α true ^  ap h' (q  s ^)  α false)})
  ... | inl q | inr s = fibres-props-eq
                        isEquiv-is-prop _ _
                        (funext λ { true  ap  Z  pr₁ (g Z) true) q  q ^
                                  ; false  ap  Z  pr₁ (g Z) false) q  s ^})
  ... | inr q | inl s = fibres-props-eq
                        isEquiv-is-prop _ _
                        (funext λ { true  ap  Z  pr₁ (g Z) true) q  q ^
                                  ; false  ap  Z  pr₁ (g Z) false) q  s ^})
  ... | inr q | inr s = fibres-props-eq
                        isEquiv-is-prop _ _
                        (funext λ { x  Empty-ind $ true-neq-false
                          (α true ^  ap h' (q  s ^)  α false)})

We can now prove the desired result.

2≃2-equiv-2 : (Bool  Bool)  Bool
2≃2-equiv-2 = equiv-adjointify (f , g , η , ϵ)

Author: James Leslie

Created: 2021-03-27 Sat 10:47