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 6 commits
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
204 changes: 162 additions & 42 deletions theories/Cubical/PathSquare.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,7 @@ Notation sq_G1 := equiv_sq_G1.
Notation sq_1G := equiv_sq_1G.

Local Open Scope equiv_scope.
Local Open Scope square_scope.
Local Open Scope path_scope.

(** [PathSquare] horizontal reflexivity *)
Expand Down Expand Up @@ -400,8 +401,6 @@ Section PathSquareConcat.
1,2: apply inverse, concat_p1.
Defined.

Infix "@@h" := sq_concat_h : square_scope.

(* Vertical concatenation of squares *)
Definition sq_concat_v {a20 a21 : A}
{py0 : a10 = a20} {py1 : a11 = a21} {p2x : a20 = a21}
Expand All @@ -414,10 +413,11 @@ Section PathSquareConcat.
1,2: apply inverse, concat_p1.
Defined.

Infix "@@v" := sq_concat_v : square_scope.

End PathSquareConcat.

Infix "@@h" := sq_concat_h : square_scope.
Infix "@@v" := sq_concat_v : square_scope.

(* Horizontal groupoid laws for concatenation *)
Section GroupoidLawsH.

Expand All @@ -431,19 +431,30 @@ Section GroupoidLawsH.
{px3 : a03 = a13} {p0z : a02 = a03} {p1z : a12 = a13}
(s : PathSquare px0 px1 p0x p1x).

Local Open Scope square_scope.
Notation hr := (sq_refl_h _).
Notation vr := (sq_refl_v _).


Definition sq_concat_h_s1 : sq_concat_h s hr = sq_ccGG (concat_p1 _)^ (concat_p1 _)^ s.
Proof.
by destruct s.
by destruct px1.
Defined.

Definition sq_concat_h_1s : sq_concat_h hr s = sq_ccGG (concat_1p _)^ (concat_1p _)^ s.
Proof.
by destruct s.
Defined.

Definition sq_concat_v_s1 : sq_concat_v s vr = sq_GGcc (concat_p1 _)^ (concat_p1 _)^ s.
Proof.
by destruct p1x.
Defined.

Definition sq_concat_v_1s : sq_concat_v vr s = sq_GGcc (concat_1p _)^ (concat_1p _)^ s.
Proof.
by destruct s.
Defined.

Context (t : PathSquare px1 px2 p0y p1y) (u : PathSquare px2 px3 p0z p1z).

Definition sq_concat_h_ss_s : sq_concat_h (sq_concat_h s t) u
Expand All @@ -468,49 +479,13 @@ Section Kan.
by destruct px1, p0x, p1x.
Defined.

Definition sq_fill_l_uniq
{px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
{px0 : a00 = a10} (s : PathSquare px0 px1 p0x p1x)
{px0' : a00 = a10} (s' : PathSquare px0' px1 p0x p1x)
: px0 = px0'.
Proof.
destruct s.
apply sq_path^-1 in s'.
exact (s'^ @ concat_p1 _).
Defined.

Definition sq_fill_r (px0 : a00 = a10) (p0x : a00 = a01) (p1x : a10 = a11)
: {px1 : a01 = a11 & PathSquare px0 px1 p0x p1x}.
Proof.
exists (p0x^ @ px0 @ p1x).
by destruct px0, p0x, p1x.
Defined.

Definition sq_fill_r_uniq
{px0 : a00 = a10} {p0x : a00 = a01} {p1x : a10 = a11}
{px1 : a01 = a11} (s : PathSquare px0 px1 p0x p1x)
{px1' : a01 = a11} (s' : PathSquare px0 px1' p0x p1x)
: px1 = px1'.
Proof.
destruct s.
apply sq_path^-1 in s'.
exact (s' @ concat_1p _).
Defined.

Definition equiv_sq_fill_lr (p0x : a00 = a01) (p1x : a10 = a11)
: (a00 = a10) <~> (a01 = a11).
Proof.
srapply equiv_adjointify.
- intros px0; exact (sq_fill_r px0 p0x p1x).1.
- intros px1; exact (sq_fill_l px1 p0x p1x).1.
- intros px1.
exact (sq_fill_r_uniq (sq_fill_r _ p0x p1x).2
(sq_fill_l px1 p0x p1x).2).
- intros px0.
exact (sq_fill_l_uniq (sq_fill_l _ p0x p1x).2
(sq_fill_r px0 p0x p1x).2).
Defined.

Definition sq_fill_t (px0 : a00 = a10) (px1 : a01 = a11) (p1x : a10 = a11)
: {p0x : a00 = a01 & PathSquare px0 px1 p0x p1x}.
Proof.
Expand All @@ -527,6 +502,151 @@ Section Kan.

End Kan.

(** To prove stronger uniqueness results and related induction principles, we need to start a new section so we can generalize over all of the points. *)

Section KanUnique.

Context {A : Type} {a00 a10 a01 a11 : A}.

#[export] Instance sq_fill_l_contr (px1 : a01 = a11) (p0x : a00 = a01) (p1x : a10 = a11)
: Contr {px0 : a00 = a10 & PathSquare px0 px1 p0x p1x}.
Proof.
apply (Build_Contr _ (sq_fill_l px1 p0x p1x)).
intros [px0' s'].
by destruct s'.
Defined.

Definition sq_fill_l_uniq {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
{px0 : a00 = a10} (s : PathSquare px0 px1 p0x p1x)
{px0' : a00 = a10} (s' : PathSquare px0' px1 p0x p1x)
: px0 = px0'
:= ap pr1 (@path_contr _ (sq_fill_l_contr px1 p0x p1x) (px0; s) (px0'; s')).

#[export] Instance sq_fill_r_contr (px0 : a00 = a10) (p0x : a00 = a01) (p1x : a10 = a11)
: Contr {px1 : a01 = a11 & PathSquare px0 px1 p0x p1x}.
Proof.
apply (Build_Contr _ (sq_fill_r px0 p0x p1x)).
intros [px1' s'].
by destruct s'.
Defined.

Definition sq_fill_r_uniq {px0 : a00 = a10} {p0x : a00 = a01} {p1x : a10 = a11}
{px1 : a01 = a11} (s : PathSquare px0 px1 p0x p1x)
{px1' : a01 = a11} (s' : PathSquare px0 px1' p0x p1x)
: px1 = px1'
:= ap pr1 (@path_contr _ (sq_fill_r_contr px0 p0x p1x) (px1; s) (px1'; s')).

#[export] Instance sq_fill_t_contr (px0 : a00 = a10) (px1 : a01 = a11) (p1x : a10 = a11)
: Contr {p0x : a00 = a01 & PathSquare px0 px1 p0x p1x}.
Proof.
apply (Build_Contr _ (sq_fill_t px0 px1 p1x)).
intros [p0x' s'].
by destruct s'.
Defined.

Definition sq_fill_t_uniq {px0 : a00 = a10} {px1 : a01 = a11} {p1x : a10 = a11}
{p0x : a00 = a01} (s : PathSquare px0 px1 p0x p1x)
{p0x' : a00 = a01} (s' : PathSquare px0 px1 p0x' p1x)
: p0x = p0x'
:= ap pr1 (@path_contr _ (sq_fill_t_contr px0 px1 p1x) (p0x; s) (p0x'; s')).

#[export] Instance sq_fill_b_contr (px0 : a00 = a10) (px1 : a01 = a11) (p0x : a00 = a01)
: Contr {p1x : a10 = a11 & PathSquare px0 px1 p0x p1x}.
Proof.
apply (Build_Contr _ (sq_fill_b px0 px1 p0x)).
intros [p1x' s'].
by destruct s'.
Defined.

Definition sq_fill_b_uniq {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01}
{p1x : a10 = a11} (s : PathSquare px0 px1 p0x p1x)
{p1x' : a10 = a11} (s' : PathSquare px0 px1 p0x p1x')
: p1x = p1x'
:= ap pr1 (@path_contr _ (sq_fill_b_contr px0 px1 p0x) (p1x; s) (p1x'; s')).

(** Induction principles that only require one edge to be free. It might be possible to use these to simplify other work involving squares, including work earlier in the file, so we could consider moving these and the material on fillers earlier in the file. *)

Definition pathsquare_ind_l
{px1 : a01 = a11}
{p0x : a00 = a01} {p1x : a10 = a11}
(P : forall (px0 : a00 = a10) (sq : PathSquare px0 px1 p0x p1x), Type)
(fill := (sq_fill_l px1 p0x p1x))
(p : P fill.1 fill.2)
: forall px0 sq, P px0 sq.
Proof.
intros px0 sq.
by destruct sq.
Defined.

Definition pathsquare_ind_r
{px0 : a00 = a10}
{p0x : a00 = a01} {p1x : a10 = a11}
(P : forall (px1 : a01 = a11) (sq : PathSquare px0 px1 p0x p1x), Type)
(fill := (sq_fill_r px0 p0x p1x))
(p : P fill.1 fill.2)
: forall px1 sq, P px1 sq.
Proof.
intros px1 sq.
by destruct sq.
Defined.

Definition pathsquare_ind_t
{px0 : a00 = a10} {px1 : a01 = a11}
{p1x : a10 = a11}
(P : forall (p0x : a00 = a01) (sq : PathSquare px0 px1 p0x p1x), Type)
(fill := (sq_fill_t px0 px1 p1x))
(p : P fill.1 fill.2)
: forall p0x sq, P p0x sq.
Proof.
intros p0x sq.
by destruct sq.
Defined.

Definition pathsquare_ind_b
{px0 : a00 = a10} {px1 : a01 = a11}
{p0x : a00 = a01}
(P : forall (p1x : a10 = a11) (sq : PathSquare px0 px1 p0x p1x), Type)
(fill := (sq_fill_b px0 px1 p0x))
(p : P fill.1 fill.2)
: forall p1x sq, P p1x sq.
Proof.
intros p1x sq.
by destruct sq.
Defined.

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