Skip to content

Instantly share code, notes, and snippets.

@ncfavier
Last active August 4, 2022 09:31
Show Gist options
  • Save ncfavier/84638aaca81d149b9c4f8f7c154c77bf to your computer and use it in GitHub Desktop.
Save ncfavier/84638aaca81d149b9c4f8f7c154c77bf to your computer and use it in GitHub Desktop.
[WIP] Equivalence between the "coherentified" version of @ice1000's Niltok type and the booleans
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) = {! !}
-- 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 _ _ _ _ _ _)
@Trebor-Huang
Copy link

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.

@ncfavier
Copy link
Author

ncfavier commented Aug 4, 2022

Downsides could also be related to verbosity and performance.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment