Cubical experiment

cubicaluib.agda

{-# OPTIONS --cubical --rewriting #-}

module _ where

open import Cubical.Core.Everything
  using (_∧_; _∨_;  ~_; i0;i1 ; transp; Σ; fst; snd
        ; Glue ; glue ; unglue ; lineToEquiv;
        _≃_; _,_)

open import Cubical.Foundations.Prelude
  using ( transportRefl
         ; _≡⟨_⟩_
         ; _∎
         ; _≡_          
         ; refl         
         ; transport
         ; hcomp    
         ; J            
         ; JRefl        
         ; sym          
         ; _∙_          
         ; cong         
         ; isContr      
         ; isProp       
         ; isSet        
         ; funExt       
         ; funExt⁻      
         ; subst        
         ; isPropIsContr
        )

open import Cubical.Foundations.Equiv
  using ( idEquiv; equivToIso; compEquiv; isPropIsEquiv
        ; equivEq ; invEq ; retEq ; secEq ; funIsEq
        ; isEquiv ; fiber )
open import Cubical.Foundations.Isomorphism
  using ( isoToEquiv; iso; Iso; isoToPath)

open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
    using ( ua             
             ; pathToEquiv    
             ; pathToEquiv-ua 
             ; ua-pathToEquiv 
             ; univalence     
             ; univalenceIso  )

open import Cubical.Data.Bool
open import Cubical.Data.Nat
open import Cubical.HITs.Susp using (Susp; north; south; merid)
open import Cubical.HITs.S1 using (S¹; base ; loop)

_-sphere : ℕ → Set 
0 -sphere = Bool 
(suc n) -sphere = Susp (n -sphere)

1-sphere-to-S1 : (1 -sphere) → S¹
1-sphere-to-S1 north = base
1-sphere-to-S1 south = base
1-sphere-to-S1 (merid false i) = base
1-sphere-to-S1 (merid true i)  = loop i

{-
     n
   /   \
f |     | t
   \   /
     s

   -------
  /       \
n/s        | t
  \       /
   -------
-}

S1-to-1-sphere : S¹ → (1 -sphere )
S1-to-1-sphere base     = south
S1-to-1-sphere (loop i) = (sym (merid false) ∙ merid true) i 

{-
     n
   /   \
f |  ↻  | t
   \   /
     s
-}


go : (b : S¹) → 1-sphere-to-S1 (S1-to-1-sphere b) ≡ b
go base       = refl
go (loop i) j = lUnit loop (~ j) i
  where
  aux : (λ j → 1-sphere-to-S1 (S1-to-1-sphere (loop j))) ≡ (refl ∙ loop)
  aux = refl

{-
                                        
              base---------base
               |             |
refl . loop    |    lUnit    | loop
               |             |
              base <--j---- base

j is x-axis
i is y-axis


forall j -> 1-sphere-to-S1 (S1-to-1-sphere (loop j)) ≡ (refl ∙ loop) j

(sym (merid false) ∙ merid true) i0,i1 == south
(refl           · loop) i  =  loop i    (after applying 1-sphere-to-S1)

1-sphere-to-S1 (S1-to-1-sphere (loop i))
=
1-sphere-to-S1 ((sym (merid false) ∙ merid true) i)
= (want)
(1-sphere-to-S1 (sym (merid false)) ∙ 1-sphere-to-S1 (merid true)) i
= (want)
(sym (1-sphere-to-S1 (merid false)) ∙ 1-sphere-to-S1 (merid true)) i
=

-}

back : (b : Susp Bool) → S1-to-1-sphere (1-sphere-to-S1 b) ≡ b
back north = sym (merid false)
back south = refl
back (merid false i) j = sym (merid false) (~ i ∧ j)
{-
merid false (~ i ∧ j0) = merid false (j0) : north = south
merid false (~ i ∧ j1) = merid false (~ i)
-- sym (merid false (~ i ∧ j1) )
-}
back (merid true i) j = 
  hcomp (λ k → λ { (i = i0) → {!    !}
                 ; (i = i1) → {!   !}
                 ; (j = i0) → {!   !}
                 ; (j = i1) → {!   !}}
                 )
            (sym (merid false) i)
        
{-


             j0                                j1
((merid false)⁻¹ ∙ merid true)   |       | merid true 
                                 south --

-}

-- lemma : 1 -sphere ≡ S¹
-- lemma = isoToPath (iso 1-sphere-to-S1 S1-to-1-sphere go back)