[WIP] Equivalence between the "coherentified" version of @ice1000's Niltok type and the booleans

Niltok-coh.agda

open import 1Lab.Type
open import 1Lab.Path
open import 1Lab.Path.Groupoid
open import Data.Bool

data Niltok : Type where
  t : Niltok
  nicht : Niltok → Niltok
  mod2 : (n : Niltok) → n ≡ nicht (nicht n)
  coh : (n : Niltok) → ap nicht (mod2 n) ≡ mod2 (nicht n)

bool-mod2 : (b : Bool) → b ≡ not (not b)
bool-mod2 false = refl
bool-mod2 true = refl

bool-coh : (b : Bool) → ap not (bool-mod2 b) ≡ bool-mod2 (not b)
bool-coh false = refl
bool-coh true = refl

to : Niltok → Bool
to t = true
to (nicht n) = not (to n)
to (mod2 n i) = bool-mod2 (to n) i
to (coh n i j) = bool-coh (to n) i j

from : Bool → Niltok
from false = nicht t
from true = t

to-from : (b : Bool) → to (from b) ≡ b
to-from false = refl
to-from true = refl

from-not : (b : Bool) → from (not b) ≡ nicht (from b)
from-not false = mod2 t
from-not true = refl

from-bool-mod2 : (b : Bool) →
  ap from (bool-mod2 b) ∙ from-not (not b) ∙ ap nicht (from-not b) ≡ mod2 (from b)
from-bool-mod2 false = ∙-id-l _ ∙ ∙-id-l _ ∙ coh t
from-bool-mod2 true = ∙-id-l _ ∙ ∙-id-r _

-- from-bool-coh : (b : Bool) →
--   Cube (λ i j → from (bool-coh b i j)) (coh (from b)) ? ? ? ?
-- from-bool-coh b = ?

from-to : (n : Niltok) → from (to n) ≡ n
from-to t = refl
from-to (nicht n) = from-not _ ∙ ap nicht (from-to n)
from-to (mod2 n i) = composite-path→square square i where
  square : ap from (bool-mod2 (to n))
         ∙ from-not (not (to n)) ∙ ap nicht (from-not (to n) ∙ ap nicht (from-to n))
         ≡ from-to n
         ∙ mod2 n
  square = ap (ap from (bool-mod2 (to n)) ∙_) (
             ap (from-not (not (to n)) ∙_) (ap-comp-path nicht _ _)
           ∙ ∙-assoc _ _ _)
         ∙ ∙-assoc _ _ _
         ∙ ap (_∙ ap (nicht ∘ nicht) (from-to n)) (from-bool-mod2 (to n))
         ∙ sym (∙-cancel-l _ _)
         ∙ ap (from-to n ∙_) (
             sym (transport-path _ _ _)
           ∙ from-pathp (ap mod2 (from-to n)))
from-to (coh n i j) = {!   !}

Niltok-squash.agda

-- This version uses a set truncation rather than bespoke coherences,
-- which makes the proof *much* simpler.
open import 1Lab.Type
open import 1Lab.Path
open import 1Lab.HLevel
open import Data.Bool

data Niltok : Type where
  t : Niltok
  nicht : Niltok → Niltok
  mod2 : (n : Niltok) → n ≡ nicht (nicht n)
  squash : is-set Niltok

bool-mod2 : (b : Bool) → b ≡ not (not b)
bool-mod2 false = refl
bool-mod2 true = refl

to : Niltok → Bool
to t = true
to (nicht n) = not (to n)
to (mod2 n i) = bool-mod2 (to n) i
to (squash n n' p p' i j) = Bool-is-set (to n) (to n') (λ i → to (p i)) (λ i → to (p' i)) i j

from : Bool → Niltok
from false = nicht t
from true = t

to-from : (b : Bool) → to (from b) ≡ b
to-from false = refl
to-from true = refl

from-not : (b : Bool) → from (not b) ≡ nicht (from b)
from-not false = mod2 t
from-not true = refl

from-to : (n : Niltok) → from (to n) ≡ n
from-to t = refl
from-to (nicht n) = from-not _ ∙ ap nicht (from-to n)
from-to (mod2 n i) = square i where
  square : Square (ap from (bool-mod2 (to n)))
                  (from-to n)
                  (from-not (not (to n)) ∙ ap nicht (from-not (to n) ∙ ap nicht (from-to n)))
                  (mod2 n)
  square = to-pathp (squash _ _ _ _)
from-to (squash n n' p p' i j) k = cube k i j where
  cube : PathP (λ k → Square refl
                             (λ j → from-to (p j) k)
                             (λ j → from-to (p' j) k)
                             refl)
               (λ i j → from (Bool-is-set (to n) (to n') (ap to p) (ap to p') i j))
               (squash n n' p p')
  cube = to-pathp (is-hlevel-suc 2 squash _ _ _ _ _ _)

Maybe we can truncate Niltok type to Set level then it can be easily proven equivalent to Bool

(Wow, didn't expect Niltok to be named after someone) yeah, that would probably be easier.

How would introducing the coh constructor compare to just brute forcing a trunc : isSet Niltok? Would there be any advantages?

Advantages, yes: the proof is now almost trivial (the mod2 case is to-pathp (trunc _ _ _ _) and the trunc case follows similarly because h-level 0 implies h-level 1).

(This makes me think that the right strategy for proving things with coh would indeed be to prove that Niltok is a set first, but actually that doesn't sound much easier than proving the equivalence directly...)

I'm not experienced enough to know if there are any drawbacks.

Added the proof with is-set. As you can see, there's more types than code (although I'm deferring to is-hlevel-suc).

According to the intro of https://arxiv.org/pdf/2007.00167.pdf, adding a set truncation means you can't eliminate into non-set types anymore.

To think of it, all the downsides should be contained in a proof that the coh-version is isomorphic to the trunc-version, since after that they are just interchangeable.

Downsides could also be related to verbosity and performance.