Tactics for characterising path types between records

[Alizter]

It ought to be a completely routine process to characterise the path type of a given record.

Is there a way we can "tag" certain functions associated to Records? For example given any record type, econstructor can work out which constructor to use. Can we create a "path tag" which allows us to have a tactic pathtactic which can prove path_data_sometype a b <~> a = b for a b : SomeType given the presence of a path_sometype function?

The reason I ask is that between any two terms of a record type, there ought to be two kinds of path spaces. A "naive one", whereby there are only equalities between the fields and the correct one, whereby fields also have their "path_somefield" functions called.

Something like this is already present in Diagrams/Diagram.v where we have path_diagram_naive and path_diagram, where the latter uses funext to construct path types of the function fields.

Now it seems to me, having a "naive path space" is doable with some modification of the issig tactic discussed in #1097. Or better yet, "issig"ing the records and using path_sigma. The "correct path space" is quite a lot more difficult however, since we would have to untangle funexts and transport along previous equalities etc.

I have created this issue so we can discuss how this might be done.

@JasonGross Any ideas?

Here is a test case that has some nasty funext, Jason kindly started it in #1093 :

Require Import Basics Types.

Record Dep3x3 := {
  B00 : Type; B04 : Type;
  B40 : Type; B44 : Type;
  B02 : B00 -> B04 -> Type;
  B42 : B40 -> B44 -> Type;
  B20 : B00 -> B40 -> Type;
  B24 : B04 -> B44 -> Type;
  B22 : forall b00 b44 b04 b40,
    B02 b00 b04 ->
    B42 b40 b44 ->
    B20 b00 b40 ->
    B24 b04 b44 -> Type;
}.

(* Notation for identity map transport. *)
Notation coe p x := (transport idmap p x).

(* Here is the data that makes up the path type of a Dep3x3. *)
Record path_dep3x3 (u v : Dep3x3) := {
  p00 : u.(B00) = v.(B00);
  p04 : u.(B04) = v.(B04);
  p40 : u.(B40) = v.(B40);
  p44 : u.(B44) = v.(B44);
  p02 : forall x y, u.(B02) x y = v.(B02) (coe p00 x) (coe p04 y);
  p42 : forall x y, u.(B42) x y = v.(B42) (coe p40 x) (coe p44 y);
  p20 : forall x y, u.(B20) x y = v.(B20) (coe p00 x) (coe p40 y);
  p24 : forall x y, u.(B24) x y = v.(B24) (coe p04 x) (coe p44 y);
  p22 : forall b00 b44 b04 b40 b02 b42 b20 b24,
    u.(B22) b00 b44 b04 b40 b02 b42 b20 b24
      = v.(B22) (coe p00 b00) (coe p44 b44) (coe p04 b04) (coe p40 b40)
        (coe (p02 b00 b04) b02)
        (coe (p42 b40 b44) b42)
        (coe (p20 b00 b40) b20)
        (coe (p24 b04 b44) b24);
}.

Definition equiv_path_dep3x3 `{Funext} {u v : Dep3x3}
  : path_dep3x3 u v <~> u = v.
Proof.
Admitted.

[SkySkimmer]

Sounds like something a plugin could do.

[mikeshulman]

If we used nested sigma-types instead of records, this could be done with typeclasses.

[Alizter]

@mikeshulman It is pretty easy to turn all the records into sigma types now. How exactly can this be done with typeclasses?

[mikeshulman]

I think I tried something like this in the past, but I can't find it now. I would define a typeclass for types that "have an equiv_path_X function", with instances for sigmas as well as functions. Then typeclass search for such an instance on a sigma-type would recursively descend into typeclass search on its arguments. And there would be a low-priority bottom-out instance that just returns the ordinary path space. IIRC there would probably be issues dealing with dependency, I'm not sure how serious.

IIRC nested sigma-types were also significantly slower than records in some places.

[Alizter]

@mikeshulman I don't see how this would work when the arguments are dependent on one another.

[mikeshulman]

Yes, as I said there would be issues. The obvious thing to do is to have the typeclass instances be type families rather than (or in addition to) single types. I don't remember how far I went down that road and whether there was an obstacle.

[Alizter]

@mikeshulman I like the idea of being able to tag types with a class however. This might give the tagging function I was looking for.

[mikeshulman]

We could also deal with record types by simply manually defining instances for them, with proofs by issign.

[JasonGross]

I think there is some code for something like this here: https://github.com/HoTT/HoTT/blob/master/theories/Tactics/EquivalenceInduction.v

[Alizter]

@mikeshulman Is the equivalence induction what you were referring to?

Also can you expand a bit more on making the typeclass instances families instead to deal with dependency?

[mikeshulman]

Maybe I was remembering equivalence induction instead, though it's not quite the same as what we're talking about here. What more are you looking for about family instances?

[Alizter]

@mikeshulman I don't know you said

The obvious thing to do is to have the typeclass instances be type families rather than (or in addition to) single types.

I don't quite understand how this lets us deal with dependency.

The Dep3x3 type I gave above is easier than most in that I have (probably) characterised the path type and I can start proving it is equivalent. I can't actually finish this proof because the funexts are kind of ridiculous here.

Here is another record type I would like to characterise the path type of:

Record Diagram3x3 : Type := {
  A00 : Type; A02 : Type; A04 : Type;
  A20 : Type; A22 : Type; A24 : Type;
  A40 : Type; A42 : Type; A44 : Type;
  f01 : A02 -> A00; f03 : A02 -> A04;
  f10 : A20 -> A00; f12 : A22 -> A02; f14 : A24 -> A04;
  f21 : A22 -> A20; f23 : A22 -> A24;
  f30 : A20 -> A40; f32 : A22 -> A42; f34 : A24 -> A44;
  f41 : A42 -> A40; f43 : A42 -> A44;
  H11 : f01 o f12 == f10 o f21; H13 : f03 o f12 == f14 o f23;
  H31 : f41 o f32 == f30 o f21; H33 : f43 o f32 == f34 o f23;
}.

Here I have no idea what it should actually look like. I can start with equating the first 9 types, but then the functions get tricky. I can pre and post compose transport with the function in order to compare them, but when I get to the homotopies I am completely lost.

The fact that I can't manage to write down this path type means I have very little chance in thinking of a tactic to do it for me. >:-)

Even if we could fully characterise path types of nested sigma types, wouldn't this mean we could fully characterise path types of W-types too. I don't know anybody who has done this to my knowledge?

[mikeshulman]

Backing up a bit, why do you want to characterize the path type of an entire 3x3 diagram? Surely that's not necessary for proving the 3x3 lemma. Generally we use equivalences and homotopies whenever feasible and only convert them back and forth to equalities of types and functions when absolutely necessary, to avoid univalence and funext redexes.

[Alizter]

My current plan is to show that the dependent 3x3 diagram and the regular 3x3 diagram are equivalent. Which ought to be the Reedy fibrant replacement. Let's call this equivalence e, which takes a dependent 3x3 diagram and gives a regular 3x3 diagram.

Now lets call the statement of the 3x3 lemma P which is a type family over 3x3 diagrams. Now proving P (e t) for some dependent diagram t should be easier than proving it directly since the diagram commutes judgementally. It ought to be a simplified version of Brunerie's proof, who spends a lot of time dealing with coherences of Kan fillers. All of this is gone now. Lets call the statement Q := forall t, P(e t).

Now all we have to do to prove forall x, P x is prove forall x, P (e (e^-1 x)).

So I see this as a way to simplify Brunerie's proof. I have managed to prove the to and from maps of the equivalence Q t. I hoped that I could do some form of double pushout induction (with dependent paths instead of transports) which gives me a cube that I have to resolve. When proving the Torus is equivalent to the product of circles, this technique worked because you could prove everything at the same time by cube concatenation.

It looks to be the case that this is not possible at the moment. I have to still use cube concatenation but only after providing each of the faces first. I have to make sure they are in a suitable form for cube concatenation to work etc.

@mikeshulman your plan with the symmetric double pushout was basically to have a middle term in this proof that might be easier to work with. I ran into the same issue there in that I need to prove a cube and I have no idea how.

If you want to see this in action, I was messing around on this branch here. You can find my attempt in Colimits/Pushout3x3.

[mikeshulman]

My point is that I think it would be better to verify directly that P is invariant under equivalences of diagrams, rather than try to make an equivalence of diagrams into a path of diagrams using univalence and funext and then just transport in P. Yesterday I would have said that the former is sure to be less work overall. With #1112 I'm no longer sure of that, but I still think the former would be better, because it avoids introducing unnecessary univalence and funext redexes.

[mikeshulman]

Can we close this issue?

[Alizter]

@mikeshulman Perhaps once we have #1120.

[mikeshulman]

But since #1120 will remain open until we do it, and is more specific than this one, do we also need this one hanging around?