Hopf Fibration

[5HT]

I don't know the current state of type checker, just want to encode S3 Hopf fibration.

loopS1 : U = Path S1 base base
loop1 : loopS1 = <i> loop{S1} @ i

mLoop : (x : S1) -> Path S1 x x = split
  base -> loop1
  loop @ i -> (constSquare S1 base loop1) @ i

rot : S1 -> S1 -> S1 = split
  base -> (\ (y : S1) -> y)
  loop @ i -> (\ (y : S1) -> mLoop y @ i)

S2 : U = susp S1
S3 : U = susp S2

fextToHE  (A B : U) (f g : A -> B) (p : Path (A -> B) f g)
                 (e1 : isEquiv A B f) (e2 : isEquiv A B g)
        : PathP (<x> isEquiv A B (p @ x)) e1 e2
        = J (A -> B) f (\ (g : A -> B)
          (p: Path (A->B) f g)->(e1: isEquiv A B f)
               (e2: isEquiv A B g)->PathP (<x>isEquiv A B (p@x)) e1 e2)
          (\(e1: isEquiv A B f) (e2: isEquiv A B f) ->
                  propIsEquiv A B f e1 e2) g p e1 e2

rotLoop : PathP (<i> isEquiv S1 S1 (rot (loop{S1}@i))) (idIsEquiv S1) (idIsEquiv S1)
        = <x>fextToHE S1 S1 (idfun S1) (idfun S1) (<i>rot (loop{S1}@i))
                                            (idIsEquiv S1) (idIsEquiv S1) @ x

rotIsEquiv: (a: S1) -> isEquiv S1 S1 (rot a)
   = split { base -> idIsEquiv S1; loop@x -> rotLoop@x }
rotpath (x: S1): Path U S1 S1 = equivPath S1 S1 (rot x) (rotIsEquiv x)

-- Hopf fibration
H : S2 -> U = split { north -> S1; south -> S1; merid a @ x -> rotpath a@x }

-- total space of H
TH : U = (c : S2) * H c

It currently stucks with

Checking: rotLoop
Type checking failed: check conv:
S1
/=
S1

[mortberg]

That sounds very strange. Can you try it on the hcomptrans branch? (HITs work correctly there)

Here is another formalization of the Hopf fibration that you can compare with: https://github.com/mortberg/cubicaltt/blob/hcomptrans/examples/brunerie.ctt#L522

[5HT]

hcomptrans failed to build:

$ stack build
Downloaded lts-11.14 build plan.
AesonException "Error in $.packages.cassava.constraints.flags['bytestring--lt-0_10_4']:
Invalid flag name: \"bytestring--lt-0_10_4\""

[mortberg]

I never use stack... It compiles fine for me with the Makefile.

[5HT]

With make it was never compiled for me, even master :-) I thought stack is a main choice.

$ make
ghc -O2 -rtsopts -v0 Connections.hs

Connections.hs:14:1: error:
    Failed to load interface for ‘Test.QuickCheck’
    Use -v to see a list of the files searched for.
GNUmakefile:43: recipe for target 'Connections.hi' failed
make: *** [Connections.hi] Error 1

[mortberg]

Try to run cabal update && cabal install QuickCheck and then run make again

[5HT]

cabal update && cabal install QuickCheck performed well on hcomptrans branch, but still failed on make:

$ make
ghc -O2 -rtsopts -v0 Connections.hs
ghc -O2 -rtsopts -v0 CTT.hs
ghc -O2 -rtsopts -v0 Eval.hs
ghc -O2 -rtsopts -v0 TypeChecker.hs

TypeChecker.hs:6:1: error:
    Failed to load interface for ‘Control.Monad.Except’
    Perhaps you meant Control.Monad.Zip (from base-4.9.1.0)
    Use -v to see a list of the files searched for.

TypeChecker.hs:7:1: error:
    Failed to load interface for ‘Control.Monad.Reader’
    Perhaps you meant Control.Monad.Fail (from base-4.9.1.0)
    Use -v to see a list of the files searched for.
GNUmakefile:40: recipe for target 'TypeChecker.hi' failed
make: *** [TypeChecker.hi] Error 1

NOTE: with master branch the same behavior.

[mortberg]

Ok, I think you need to install mtl. The README says:

This assumes that the following Haskell packages are installed using cabal:

  mtl, haskeline, directory, BNFC, alex, happy, QuickCheck

[5HT]

Today is not my day:

$ cabal install mlt haskeline directory BNFC alex happy QuickCheck
...
Building haskeline-0.7.4.2...
Installed alex-3.2.4
Installed happy-1.19.9
Installed haskeline-0.7.4.2
cabal: Error: some packages failed to install:
BNFC-2.8.1 failed during the configure step. The exception was:
ExitFailure 1

[mortberg]

Wow, I don't think I can help you with that... Maybe using stack is easier, but I don't know how to fix the error you were getting either...

[5HT]

I've built, but seems my library is incompatible with hcomptrans branch. Need to porting.

P.S. The problem was 1) cabal install doesn't handle correctly multiple targets in the same line. 2) sudo apt install bnfc alex happy

[5HT]

Now about the subject:

1) in master branch Brunerie's Hopf through mu also doesn't check. Same style of error S1 =/ S1 2) in hcomptrans I've made a self-contained file (200 LOC) from Brunerie's Hopf [1] and it's stuck at:

Checking: ua
Checking: mu
  Checking: f
  Checking: goal

I waited a while (30min), but don't know when it ends (seems like hidden U : U issue in mu)

[1] https://github.com/groupoid/infinity/blob/master/priv/hopf.ctt

Could you take a look?

Actually I'm looking for a confirmation that Hopf fibration could be type checked in any branch among master/cubicaltt, hcomptrans/cubicaltt, master/yacctt. The last one I only left to check :-)

/cc @guillaumebrunerie

[mortberg]

It works on hcomptrans if you make propIsEquiv opaque (just add opaque propIsEquiv before mu). You can make it transparent again later by adding transparent propIsEquiv.