Skip to content

An interchange law for squares and cleanups to Cubical/PathSquare.v #2328

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jdchristensen merged 9 commits into from
Nov 25, 2025
+247 −120
Merged

An interchange law for squares and cleanups to Cubical/PathSquare.v #2328

Changes from 1 commit
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
b0825d7
PathSquare: move Infix notations out of Section
jdchristensen Nov 20, 2025
357e2cb
PathSquare: use square scope throughout file
jdchristensen Nov 24, 2025
b2dc979
PathSquare: add sq_concat_v_s1 and _1s
Nov 24, 2025
f8208d5
PathSquare: remove equiv_sq_fill_lr (same as equiv_concat_lr)
jdchristensen Nov 24, 2025
af80708
PathSquare.v: add stronger uniqueness results for Kan Fillers
jdchristensen Nov 24, 2025
77da1c5
PathSquare: add interchange law for horizontal/vertical composition
jdchristensen Nov 24, 2025
f8050d4
PathSquare: move equiv_sq_prod later to not interrupt ap section
jdchristensen Nov 24, 2025
645de1e
PathSquare: fix comment style, update contents, etc.
jdchristensen Nov 24, 2025
a3d559c
PathSquare: add unicode figure and << >> markers
jdchristensen Nov 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 31 additions & 0 deletions theories/Cubical/PathSquare.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -616,6 +616,37 @@ Section KanUnique.

End KanUnique.

(** Interchange law. *)
Copy link
Collaborator

@Alizter Alizter Nov 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here is a diagram that may aid readers:

        h0i          h0j
   a00 ━━━━━━━━ a01 ━━━━━━━━ a02
    ┃            ┃            ┃
    ┃  sq00      ┃  sq01      ┃
vi0 ┃        vi1 ┃            ┃ vi2
    ┃            ┃            ┃
    ┃   h1i      ┃   h1j      ┃
   a10 ━━━━━━━━ a11 ━━━━━━━━ a12
    ┃            ┃            ┃
    ┃  sq10      ┃  sq11      ┃
vj0 ┃        vj1 ┃            ┃ vj2
    ┃            ┃            ┃
    ┃   h2i      ┃   h2j      ┃
   a20 ━━━━━━━━ a21 ━━━━━━━━ a22

Copy link
Collaborator

@jdchristensen jdchristensen Nov 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice! I've added that, including the unicode, with << >> markers. Let's see how it looks in the generated documentation. @Alizter Can you remind me where I can find the coqdoc/alectryon documentation that the CI generates?

Copy link
Collaborator

@Alizter Alizter Nov 24, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not possible to view it in the CI for a PR (online), but the main CI will upload and host the artefacts. Links to the hosted docs are on the wiki https://github.com/HoTT/Coq-HoTT/wiki

Copy link
Collaborator

@Alizter Alizter Nov 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you go to the specific CI job there is an upload artifact step which gives you a link to download the produced docs. That's technically one way you can view it.

Copy link
Collaborator

@Alizter Alizter Nov 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see the diagram in the recent commit btw, did you push it?

Copy link
Collaborator

@jdchristensen jdchristensen Nov 25, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Whoops, I only commited part of the changes I made. I just force pushed to fix the last commit.

Copy link
Collaborator

@jdchristensen jdchristensen Nov 25, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can just merge this once @marcbezem takes a look, and then check the documentation at that point.

Definition sq_interchange {A}
{a00 a10 a20 a01 a11 a21 a02 a12 a22 : A} (* 9 points in big square of 2x2 squares *)
(* sq00, top left, 4 paths *)
(vi0 : a00 = a10) (* i = 0,1 *)
(h0i : a00 = a01)
(vi1 : a01 = a11)
(h1i : a10 = a11)
(* sq10, bottom left, 3 paths, h1i shared with sq00 *)
(vj0 : a10 = a20) (* j = 1,2 *)
(vj1 : a11 = a21)
(h2i : a20 = a21)
(* sq01, top right, 3 paths, vi1 shared with sq00 *)
(vi2 : a02 = a12)
(h0j : a01 = a02)
(h1j : a11 = a12)
(* sq11, bottom right, 2 paths, vj1 shared with sq10 and h1j with sq01 *)
(vj2 : a12 = a22)
(h2j : a21 = a22)
(sq00 : PathSquare vi0 vi1 h0i h1i)
(sq10 : PathSquare vj0 vj1 h1i h2i)
(sq01 : PathSquare vi1 vi2 h0j h1j)
(sq11 : PathSquare vj1 vj2 h1j h2j)
: (sq00 @@v sq10) @@h (sq01 @@v sq11) = (sq00 @@h sq01) @@v (sq10 @@h sq11).
Proof.
destruct sq00, sq11.
destruct vi2, h2i.
revert vj0 sq10; rapply pathsquare_ind_l.
reflexivity.
Defined.

(* Apply a function to the sides of square *)
Definition sq_ap {A B : Type} {a00 a10 a01 a11 : A} (f : A -> B)
{px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
Expand Down