Conversion bug with glue systems?

[tomjack]

In this example, normalizing a term (transposeInvGlue) results in a term (transposeInvGlueNorm) which doesn't typecheck, due to an apparently spurious incompatible system error.

I noted that the (keys ts == keys ts') check in conv for System is the direct cause, but haven't understood the problem any further.

module convgluebug where

Path (A : U) (x y : A) : U = PathP (<i> A) x y
fiber (A B : U) (f : A -> B) (y : B) : U = (x : A) * Path B y (f x)
isContr (A : U) : U = (x : A) * ((y : A) -> Path A x y)
isEquiv (A B : U) (f : A -> B) : U = (y : B) -> isContr (fiber A B f y)
equiv (A B : U) : U = (f : A -> B) * isEquiv A B f

-- probably there is a simpler way to show the issue, but this is how I found it...
transposeInv (A : U) (x : A) (p : Path (Path A x x) (<_> x) (<_> x))
  : Path (Path (Path A x x) (<_> x) (<_> x)) 
         (<j k> p @ k @ j)
         (<j k> p @ -j @ k)
  = <i j k> comp (<_> A) (p @ ((-j /\ k) \/ (i /\ -j) \/ (-i /\ k))
                            @ ((j /\ k) \/ (-i /\ j) \/ (i /\ k)))
              [ (i=0) -> <_> p @ k @ j
              , (i=1) -> <_> p @ -j @ k
              , (j=0) -> <l> p @ (i \/ k \/ l) @ (i /\ k)
              , (j=1) -> <l> p @ (-i /\ k /\ -l) @ (-i \/ k)
              , (k=0) -> <l> p @ (i /\ -j /\ -l) @ (-i /\ j)
              , (k=1) -> <l> p @ (-i \/ -j \/ l) @ (i \/ j)
              ]

transposeInvGlue (A : U) (e : equiv A A)
  : Path (Path (Path U A A) (<_> A) (<_> A))
         (<i j> Glue A [ (i=0) -> (A, e)
                       , (i=1) -> (A, e)
                       , (j=0) -> (A, e)
                       , (j=1) -> (A, e)
                       ])
         (<i j> Glue A [ (i=0) -> (A, e)
                       , (i=1) -> (A, e)
                       , (j=0) -> (A, e)
                       , (j=1) -> (A, e)
                       ])
  = transposeInv U A
      (<i j> Glue A [ (i=0) -> (A, e)
                    , (i=1) -> (A, e)
                    , (j=0) -> (A, e)
                    , (j=1) -> (A, e)
                    ])

-- transposeInvGlueNorm below is the normal form of transposeInvGlue,
-- prettified, but it gives an incompatible system error:

-- a0 = Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ]
-- t0alpha = Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (j = 1)(k = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ]

-- those terms _do_ convert if we write them directly, though:

a0 (A : U) (e : equiv A A) 
  : Path (Path (Path U A A) (<_> A) (<_> A))
         (<j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ])
         (<j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ])
  = <i j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ]

t0alpha (A : U) (e : equiv A A)
  : Path (Path (Path U A A) (<_> A) (<_> A))
         (<j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ])
         (<j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ])
  = <i j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (j = 1)(k = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ]

hmm (A : U) (e : equiv A A)
  : Path (Path (Path (Path U A A) (<_> A) (<_> A))
               (<j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ])
               (<j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ]))
         (a0 A e) (t0alpha A e)
  = <_> a0 A e

transposeInvGlueNorm (A : U) (e : equiv A A)
  : Path (Path (Path U A A) (<_> A) (<_> A))
         (<i j> Glue A [ (i=0) -> (A, e)
                       , (i=1) -> (A, e)
                       , (j=0) -> (A, e)
                       , (j=1) -> (A, e)
                       ])
         (<i j> Glue A [ (i=0) -> (A, e)
                       , (i=1) -> (A, e)
                       , (j=0) -> (A, e)
                       , (j=1) -> (A, e)
                       ])
  = <i j k> comp (<_> U) (Glue A [ (i = 0)(j = 0) -> (A,e)
                                 , (i = 0)(j = 1) -> (A,e)
                                 , (i = 0)(k = 0) -> (A,e)
                                 , (i = 0)(k = 1) -> (A,e)
                                 , (i = 1)(j = 0) -> (A,e)
                                 , (i = 1)(j = 1) -> (A,e)
                                 , (i = 1)(k = 0) -> (A,e)
                                 , (i = 1)(k = 1) -> (A,e)
                                 , (j = 0)(k = 0) -> (A,e)
                                 , (j = 0)(k = 1) -> (A,e)
                                 , (j = 1)(k = 0) -> (A,e)
                                 , (j = 1)(k = 1) -> (A,e)
                                 ])
              [ (i = 0) -> <l> Glue A [ (j = 0) -> (A,e)
                                      , (j = 1) -> (A,e)
                                      , (k = 0) -> (A,e)
                                      , (k = 1) -> (A,e)
                                      ]
              , (i = 1) -> <l> Glue A [ (j = 0) -> (A,e)
                                      , (j = 1) -> (A,e)
                                      , (k = 0) -> (A,e)
                                      , (k = 1) -> (A,e)
                                      ]
              , (j = 0) -> <l> Glue A [ (i = 0) -> (A,e)
                                      , (i = 1) -> (A,e)
                                      , (k = 0) -> (A,e)
                                      , (k = 1) -> (A,e)
                                      , (l = 1) -> (A,e)
                                      ]
              , (j = 1) -> <l> Glue A [ (i = 0) -> (A,e)
                                      , (i = 1) -> (A,e)
                                      , (k = 0) -> (A,e)
                                      , (k = 1) -> (A,e)
                                      , (l = 1) -> (A,e)
                                      ]
              , (k = 0) -> <l> Glue A [ (i = 0) -> (A,e)
                                      , (i = 1) -> (A,e)
                                      , (j = 0) -> (A,e)
                                      , (j = 1) -> (A,e)
                                      , (l = 1) -> (A,e)
                                      ]
              , (k = 1) -> <l> Glue A [ (i = 0) -> (A,e)
                                      , (i = 1) -> (A,e)
                                      , (j = 0) -> (A,e)
                                      , (j = 1) -> (A,e)
                                      , (l = 1) -> (A,e)
                                      ]
              ]

[simhu]

Thanks for the bugreport! This should be fixed now. It turned out that the invariant for systems to only keep the maximal components was not preserved by one of the most primitve operations for systems..