Cubical/PathSquare.v: edit diagram in comment + formulate interchange lemma

[marcbezem]

1. Please take a look at the edited diagram at the beginning of PathSquare.v, fixing Confusion of orientation in Cubical/PathSquare.v #2324.
2. I added a formulation of an interchange lemma at the end.
   2a. (minor) I didn't get the infix operators @@h, @@v to work.
   2b. Just before Admitted, the proof state is:

1 goal
A : Type
x : A
h2i, vi2 : x = x
sq10 : PathSquare 1 1 1 h2i
sq01 : PathSquare 1 vi2 1 1
______________________________________(1/1)
sq_concat_h (sq_concat_v 1%square sq10) (sq_concat_v sq01 1%square) =
sq_concat_v (sq_concat_h 1%square sq01) (sq_concat_h sq10 1%square)

My plan would be the following. Through equiv_sq_path and some easy path algebra, the sq-variables correspond to 2-paths between 1 : x=x and h2i, vi2, respectively. The latter are also variables, so we can do path induction on the 2-paths and assume they are reflexivity paths. In that case the sq-variables correspond both to a 1%square and the goal can be solved by reflexivity.

I'm new to this library, so I have difficulties getting this idea to work. Any help will be appreciated, both regarding the formulation of the interchange lemma and the feasibility of my idea to prove it.

[jdchristensen]

The following gets you a bit further:

Proof.
  destruct sq00, sq11.
  destruct vi2, h2i.
  simpl.
  rewrite (sq_concat_h_1s (p0y:=1) (p1y:=1) sq01).
  simpl.
  (* We're missing the analogous [sq_concat_v_1s].  Even with it, it's not clear to me how to proceed. *)
Admitted.

The reason I choose to destruct vi2 and h2i on the second line is that the definition of the horizontal and vertical compositions uses concat_p1, so we want to destruct the paths that appear there, so that concat_p1 computes to refl. Then we have a computation law for horizontal composition of sq_refl on the left. We're missing the corresponding result for vertical composition. Even if we had it, I'm not sure what I would do next.

I've basically never used this part of the library. Maybe @Alizter has more ideas?

[Alizter]

I don't recall much of the details here, but what I do recall is that you need to shift some of the data around using naturality squares before it fully collapses. You can find a similar kind of manipulation in https://github.com/HoTT/Coq-HoTT/blob/master/theories/Homotopy/Syllepsis.v. There we aren't using the same kind of square but an equivalent one.

[marcbezem]

Thanks for the help! I added experimental to substantiate my idea. Sorry I can't express myself in terms of the library -- very simple things such as destruct (g x p) as gxp eqn:H.didn't work (but I found a work around,
after some struggle). Here is the code, which I also pushed:

Definition experimental {A}
(a : A)
(P : A -> Type)
(f : forall (x : A), (a = x) -> P(x))
(g : forall (x : A), P(x) -> (a = x))
(fxgxid: forall (x : A) (p : P x), (p = f x (g x p)))
:
forall (x : A)(p : P x), p = transport P (g x p) (f a 1).

Proof.
  intros.
  remember (g x p) as gxp eqn:H.
  destruct gxp. (* Syntax error: destruct (g x p) as gxp eqn:H.  *)
  simpl. (* Here you see that p = f a 1 if g a p = 1 *)
  destruct H.
  apply fxgxid.
Defined.

The idea is that, when applied with equiv_sq_path for f and its
inverse for g, this gives us that the sqs are 1-squares in the base case of the
path induction.

[Alizter]

Sorry I can't be more helpful here but https://github.com/HoTT/Coq-HoTT/blob/master/theories/Types/Paths.v has the lemmas you are probably after.

[jdchristensen]

@marcbezem Your experimental looks a lot like equiv_path_ind in Basics/Equivalences.v, so maybe that can help you. There is also related material in Homotopy/IdentitySystems.v.

It might also be useful to use equiv_sq_path to convert all of the squares to path equalities, and just deal with the path algebra. But then you'd need a lemma about how equiv_sq_path interacts with horizontal and vertical composition. (Which makes me wonder if we'd be better off defining squares to be path types...)

[Alizter]

I'm in favour of defining squares as path types. The only advantage of doing things this way is the auto-generated induction principle. But that's not nearly as convenient as it looks.

I would also be in favour of using the general stuff about squares we have in WildCat for squares in 1-groupoids. In fact, I don't think there is anything special about paths except for the eliminator.

[jdchristensen]

2a. (minor) I didn't get the infix operators @@h, @@v to work.

Those notations are defined within a Section, and notations don't persist outside of the section they are defined in. And it seems that Notation and Infix don't support #[export] or Global. So those notations should be moved to right after the Section closes. The hr notation is maybe too short to export globally, so it should remain in its section.

[jdchristensen]

I don't know how hard it would be to redo PathSquare.v with squares defined using path types. One advantage would be that it would be compatible with what is done in Syllepsis.v, so that duplication could be removed. It would also mean that in other situations in which a square of paths appeared, one could apply a fact from PathSquare without having to go across the equivalence.

I'm surprised that there aren't more tricks for using the current definition efficiently, but it seems hard to use the induction principle multiple times when squares share edges. I think what is needed is a separate induction principle that reduces a general square to one of the form p p 1 1 (or 1 1 p p), but I don't see how to do that in a way that will compute well. Another thing that would help would be if one of concat_1p and concat_p1 was reflexivity.

About generalizing to any 1-category using WildCat/Square.v (regarding a type as a 1-category whose 1-cells are paths), that's an interesting idea. It's probably tricky to do for someone who doesn't know the wild category library well, and may require lemmas analogous to those in PathGroupoids, so it would be additional work.

[Alizter]

@marcbezem If you could split the changes fixing the diagram at the top, we can merge that quicker. The work-in-progress is welcome to stay here as you work further on it.

Let me know if you need any advice on how to do that with git.

[marcbezem]

See #2327. If that one is OK I didn't need help with git, but thanks anyway!

Rethinking the way I did this: perhaps that has resulted in a more complicated commit history than necessary. I created a new branch and switched to it, deleted the interchange playground, committed and pushed and PR-ed from the new branch. It would perhaps have been better to go back a few commits on the new branch, and then PR from there (making sure all edits of the diagram are there).

[Alizter]

@marcbezem I think both PRs were using the same branch which is why this is showed as merged. Could you open a new draft PR in a separate branch from master on your fork with the commits you had?

[marcbezem]

Do you mean, single-topic PRs are preferred (I understand), so I open a new one about interchange, after which we cancel this multi-topic PR?

[Alizter]

@marcbezem Generally PRs focusing on one particular issue or addition are easier to review and merge since my time budget is limited. If you have a bunch of loosely related changes that's fine too.

Here we have a GitHub bug. The other PR had the same commits and made this PR be considered merged. That wasn't my intention with merging #2327. What you will have to do is re-introduce the experiment you had the end, which is evidently now in the commit history. If you make a PR for that we can continue the discussion of how best to finish the goal there.