composition in path types

[ecavallo]

import path

let experiment (A : type) (u : A) : (p : Path A u u) -> Path (Path A u u) p p =
  lam p i -> 
    comp 0 1 p [
    | i=0 => lam j -> p
    | i=1 => lam j -> p
    ] 

raises Failure("Extension subtype: nope"). If you replace the p's in the comp with holes, you can see something weird is happening to the extension types.

[jonsterling]

@ecavallo I think the goals are actually correct; the problem is the right now, the subtyping theory for extension types is a bit impoverished, so there are times when you need to eta expand a neutral element of one extension type to see that it is an element of another extension type.

This example works if you replace p in each case with lam k -> p k.

[jonsterling]

The more complicated systems that you see in the goals if you put a hole in there are induced by the boundary of the outer path type.

[ecavallo]

I think I see what you mean, but the goals still don't seem right to me. In the i=0 face the goal is
⊢ ((# <i> A [i=0 u] [i=1 u] [0=0 (@ p i)] [0=1 -]) [j=0 p])
which doesn't seem right, as the 0=0 face says the path has to be constant p. If I eta expand but replace the i=0 face with something other than constant p:

import path

let experiment (A : type) (u : A)
  : (p : Path A u u) -> (q : Path (Path A u u) p p) -> Path (Path A u u) p p
  =
  lam p q i -> 
    comp 0 1 (lam k -> p k) [
    | i=0 => lam j k -> q j k
    | i=1 => lam j k -> p k 
    ] 

then I get Failure("spine mismatch").

[jonsterling]

I see what you mean... It looks like there may be a bug somewhere 😆

[jonsterling]

My hypothesis is that we have a dimension binding issue.

[jonsterling]

I'm hoping that the issue lies with the elaborator rather than with the core, but we will see.

[jonsterling]

@ecavallo I'm going through it now, and now I am less confident that there is a bug, though I admit there is behavior that seems unexpected (to be clear, I believe there may be a bug, but I'm having trouble convincing myself of it.) Your second example is combinatorially a bit too complex for me to really get down with mentally, so let me stick with the seemingly incorrect goals emitted by the first example. If the first example exhibits a bug, then it should be possible to step through the reasoning that I give below and indicate where I went wrong.

We are trying to prove Path (Path A u u) p p. Abstracting the dimension i, we have the following goal (I instrumented redtt to print out unique identifiers, to avoid name confusion):

  i10763 : dim
  ⊢ ((# <i> A10650 [i=0 u10652] [i=1 u10652])
     [i10763=0 p10762] [i10763=1 p10762])

What this means, is that in context i..., we want to have a path between u and itself, such that this path is p when i=0 and also p when i=1. This is the correct subgoal (it's just the path introduction rule).

Next, we want to establish this goal using a composition. Now, composition doesn't immediately apply to such a goal (a restriction type!), but the elaborator knows how to transform the goal into something equivalent which does have composition. In particular, we can push the restriction in, in order to get an extension type in which we can compose. So, the goal is transformed to the following:

(# <i>
      A10650
      [i=0 u10652]
      [i=1 u10652]
      [i10763=0 (@ p10762 i)]
      [i10763=1 (@ p10762 i)])

Please note that i in the above is the dimension bound the extension type, and i10763 is the ambient i that we abstracted when introducing the outer path type, using lam i ->.

Now, we will try to compose in this extension type along the extents i10763=0 \/ i10763=1. The first goal is the cap, which has the exact same type as above. The next two goals are to construct the tube, and these will be of a restricted extension type; the restriction of the first ensures compatibility with the cap, and the restriction of the second ensures compatibliity with the cap and the first component of the tube. If I put (lam j -> p j) in for the cap, the first component of the tube has the following type goal:

   i10763 : dim,
   i10763 = 0
  ⊢ (# <x0>
        (# <i> A10650 [i=0 u10652] [i=1 u10652] [0=0 (@ p10762 i)] [0=1 -])
        [x0=0 p10762])

Let's understand what this means. The goal is an extension (pre)type of extension types. The outer extension is because the tube of a composition binds a dimension; its restriction x0=p10762 is to ensure compatibility with the cap, which was just p10762. The interior extension type is actually just identical to the original main goal, except reindexed by the restriction i10763=0. That's why we see this constant 0=0 clause! This is just the i10763=0 clause that we had before, which was induced by the path introduction rule, except that we are now under that restriction already (because this was the i10763=0 face of the composition).

I could go further, but above we have already seen why there is a constant 0=0 face in the goal, so it should suffice to find the error in what I have written above in order to better understand what is going wrong.

[ecavallo]

Hm, I think I'm starting to see what the problem is. But first, can you explain why

let experiment (A : type) (u : A) : Path A u u =
  lam i -> 
    comp 0 1 ?cap [
    | i=0 => lam j -> ?left
    | i=1 => lam j -> ?right
    ] 

raises

Encountered error:
    u
    ≠
    (@
     (! (@
         ((%5506 ((up (U kan 0) A []))<[1/%5691]>)
          ((up (up (U kan 0) A []) u []))<[1/%5691]>)
         0))
     1)

while

let experiment2 (A : type) (u : A) (p : Path A u u) : Path (Path A u u) p p =
  lam i -> 
    comp 0 1 ?cap2 [
    | i=0 => lam j -> ?left2
    | i=1 => lam j -> ?right2 
    ] 

(which is the same thing but with A instantiated with a path type) doesn't raise an error?

[ecavallo]

May be pointing out something known here, but the "extension type in which we can compose" isn't Kan (though I guess it has hcom?) because it includes equations on dimension variables it doesn't bind.

I think I have some idea what the right behavior here is, leaving for campus now and then I'll write something up.

[jonsterling]

Ahh, you're quite right about that extension "type". We should change the behavior to be less clever.

[ecavallo]

Ok, I suspect that the cleverness is the issue. Without that, I assume it would behave like experiment term in my second-to-last comment: doesn't play well with holes, but does typecheck when everything is filled in (which is better than the current behavior). The problem as it is now is that, even if the extension type were Kan, it's not the type we want to compose in: we want to compose a bunch of things that don't satisfy the restrictions to get something that does.

I guess you have probably thought more than I have about how best to propagate restrictions into comp. Seems tricky...

[jonsterling]

@ecavallo I think that we should retreat to pushing restrictions only through pi types (and later sigma, but not yet for certain reasons); and not extension type.

[ecavallo]

The same kind of unexpected behavior happens with pi types:

let experiment3 (A : type) (B : A -> type) (u : (a : A) -> B a) : Path ((a : A) -> B a) u u =
  lam i ->
    comp 0 1 u [
    | i=0 => lam j -> u
    | i=1 => lam j -> u
    ]

raises Failure("Restriction type is not Kan").

[jonsterling]

Wouldn't it be nice if we could get rid of restriction types entirely?