-
-
Save ncfavier/84638aaca81d149b9c4f8f7c154c77bf to your computer and use it in GitHub Desktop.
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 _ _ _ _ _ _) |
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.
How would introducing the
coh
constructor compare to just brute forcing atrunc : isSet Niltok
? Would there be any advantages?