[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 _ _ _ _ _ _)

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.