Canonicity failure for Z from recursive path constructors

[tomjack]

This example is the simplest reproduction I have found so far.

[tomjack]

Here is a much simpler example which seems related:

module noncanon5 where

Id (A : U) (a0 a1 : A) : U = IdP (<i> A) a0 a1

data Unit
  = inctt
  | squash (x y : Unit) <i> [(i=0) -> x, (i=1) -> y]

inctt' : Unit = transport (<_> Unit) inctt

path : Id Unit inctt' inctt'
  = <i> transport (<_> Unit) (squash{Unit} inctt inctt @ i)

-- Checking: path

test : Id Unit (path @ 0) (path @ 1)
  = <_> inctt'

-- Checking: test
-- Type checking failed: path endpoints don't match for inctt',
-- got (hComp Unit inctt [],hComp Unit inctt []), 
-- but expected (hComp Unit (hComp Unit inctt []) [],hComp Unit (hComp Unit inctt []) [])

It seems the problem is that transps used by transpHIT is implemented in terms of comp, but this doesn't match the definition of transp for squash in face.pdf.

I guess the issue should be called "new feature: support recursive path constructors".

[coquand]

Thanks for this very simple example!

When writing the rules for propositional truncation, we discovered
that the implementation of recursive HIT is not correct. The problem
here should be in transpHIT in the constructor case, VPCon c _ ws0 phis
one should call the function transpHIT for ws0 and not the function transps.
So we should remember what are the recursive argument of a constructor.

On 01 Mar 2016, at 08:00, Tom Jack notifications@github.com wrote:

Here is a much simpler example which seems related:

module noncanon5 where

Id (A : U) (a0 a1 : A) : U = IdP ( A) a0 a1

data Unit
= inctt
| squash (x y : Unit) [(i=0) -> x, (i=1) -> y]

inctt' : Unit = transport (<_> Unit) inctt

path : Id Unit inctt' inctt'
= transport (<_> Unit) (squash{Unit} inctt inctt @ i)

-- Checking: path

test : Id Unit (path @ 0) (path @ 1)
= <_> inctt'

-- Checking: test
-- Type checking failed: path endpoints don't match for inctt',
-- got (hComp Unit inctt [],hComp Unit inctt []),
-- but expected (hComp Unit (hComp Unit inctt []) [],hComp Unit (hComp Unit inctt []) [])
—
Reply to this email directly or view it on GitHub #35 (comment).

[simhu]

Yes, indeed, thanks Tom for the bug report! As Thierry mentioned we
stumbled upon this problem a while ago but never found time to think
more about it (in the general case). As I see it right now, I think
transpHIT/squeezeHIT should be a function by recursion on the type,
but this gets rather complicated.

I am still not sure if the first example you gave is the same bug,
since the output looks like it is not well typed. The term "glueElem
.." is not of type Z but of type comp^i U Z [].

[tomjack]

Thanks. I had thought e.g. the truncations were supposed to work now.

It looks like the same 'bug' to me. If you apply this diff, the example is fixed (along with my real example). For types like Q with no parameters and only recursive arguments, this seems maybe conveniently correct. :)

However.. I tried to define transp for the hub-spoke truncation, and accidentally wrote down the non-recursive pseudotruncation (as Nicolai Kraus calls it), but noticed that what I got still did not seem to make sense.

Things seem better than in the recursive case, but it seems you can still produce 'noncanonical integers'. I guess this is not the same bug? The example uses only the following HITs:

data S1 = base
        | loop <i> [(i=0) -> base, (i=1) -> base]

data S2
  = base
  | surf <i j> [ (i=0) -> base
               , (i=1) -> base
               , (j=0) -> base
               , (j=1) -> base
               ]

data punc1 (A : U)
  = inc (a : A)
  | hub (r : S2 -> A)
  | spoke (r : S2 -> A) (x : S2)
      <i> [ (i=0) -> inc (r x)
          , (i=1) -> hub r
          ]

[coquand]

Thanks again for this other simple example.
We have been mainly working on the presentation of the type system (for HIT
spheres and propositional truncation) and did not try yet to fix the bugs
for HITs (we fixed bugs last month for computing the normal form of the proof of
univalence though).
But we should try to fix the program so that it works for at least non recursive
HIT. The case VHComp for the squeezeHIT function does not seem correct
and (as noticed by Anders) the name j should also be fresh w.r.t. i in the functions
transpHIT and squeezeHIT.

On 02 Mar 2016, at 17:14, Tom Jack notifications@github.com wrote:

Thanks. I had thought e.g. the truncations were supposed to work now.

It looks like the same 'bug' to me. If you apply this diff https://www.refheap.com/db5c199451a9079c0c898645d/raw, the example is fixed (along with my real example). For types like Q with no parameters and only recursive arguments, this seems maybe conveniently correct. :)

However.. I tried to define transp for the hub-spoke truncation, and accidentally wrote down the non-recursive pseudotruncation (as Nicolai Kraus calls it), but noticed that what I got still did not seem to make sense.

Things seem better than in the non-recursive case, but it seems you can still produce 'noncanonical integers' https://www.refheap.com/de854fcc29a21291370fc850f/raw. I guess this is not the same bug? The example uses only the following HITs:

data S1 = base
| loop [(i=0) -> base, (i=1) -> base]

data S2
= base
| surf [ (i=0) -> base
, (i=1) -> base
, (j=0) -> base
, (j=1) -> base
]

data punc1 (A : U)
= inc (a : A)
| hub (r : S2 -> A)
| spoke (r : S2 -> A) (x : S2)
[ (i=0) -> inc (r x)
, (i=1) -> hub r
]
—
Reply to this email directly or view it on GitHub #35 (comment).

[simhu]

We just pushed a patch which should solve the issue for non-recursive HITs.

The issue concerning the arguments of a vpcon in squeezeHIT/transpHIT is still open though. (But I was thinking that we could maybe have a hack to get some interesting special cases to work by case distinction on the type in squeezes.)