PathSquare.v

From HoTT Require Import Basics.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Paths Types.Prod.
Require Import DPath.

Declare Scope square_scope.
Delimit Scope square_scope with square.

Local Unset Elimination Schemes.

(** * Homogeneous squares *)

(** Squares are fillers in diagrams of the following form:

<<
        a00 ----p0i---- a01
         |               |
         |         >     |
        pi0      =     pi1
         |     =         |
         |               |
        a10-----p1i-----a11
>>

Indexing of points in a square follows the convention for matrices, first a row index, then a column index. Unless stated otherwise, paths are oriented in the direction of increasing index i (or x, etc). The stylized 2-path on the antidiagonal goes from [pi0 @ p1i] to [p0i @ pi1], complying with the definition of [equiv_sq_path] below. *)

(** Contents:

  * Definition of [PathSquare] and basic properties
  * Degenerate [PathSquare]s as paths between paths
  * Flipping squares horizontally and vertically
  * [PathSquare] transpose
  * [PathSquare] inverse
  * [PathSquare] rotations
  * Edge rewriting
  * Concatenation and groupoid laws
  * Kan fillers and uniqueness, induction principles requiring only one free edge
  * Interchange law
  * Squares arising from [ap]
  * [PathSquare]s respect products
*)

(** Definition of [PathSquare left right up down]. *)
Cumulative Inductive PathSquare {A} : forall a00 {a10 a01 a11 : A},
  a00 = a10 -> a01 = a11 -> a00 = a01 -> a10 = a11 -> Type
  := sq_id : forall {x : A},
    PathSquare x 1 1 1 1.

Arguments sq_id {A x}.
Arguments PathSquare {A _ _ _ _}.
Notation "1" := sq_id : square_scope.

(** TODO: ": rename" is needed because the default names changed in Rocq 9.2.0.  When the minimum supported version is >= 9.2.0, the ": rename" can be removed. *)
(** register=no: otherwise the scheme confuses the make_equiv tactic. When the minimum supported version is >= 9.2.0, the warning can be re-enabled. *)
#[warnings="-unsupported-attributes",register=no] Scheme PathSquare_ind := Induction for PathSquare Sort Type.
Arguments PathSquare_ind {A} P f {_ _ _ _ _ _ _ _} _ : rename.
#[warnings="-unsupported-attributes",register=no] Scheme PathSquare_rec := Minimality for PathSquare Sort Type.
Arguments PathSquare_rec {A} P f {_ _ _ _ _ _ _ _} _ : rename.

(** [PathSquare_ind] is an equivalence, similar to how [paths_ind] is. *)
Instance isequiv_PathSquare_ind `{Funext} {A}
  (P : forall (a00 a10 a01 a11 : A) (p : a00 = a10) (p0 : a01 = a11)
    (p1 : a00 = a01) (p2 : a10 = a11),
    PathSquare p p0 p1 p2 -> Type) : IsEquiv (PathSquare_ind P).H: Funext
A: Type
P: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01)
(p2 : a10 = a11), PathSquare p p0 p1 p2 -> Type
IsEquiv (PathSquare_ind P)
Proof.H: Funext
A: Type
P: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01)
(p2 : a10 = a11), PathSquare p p0 p1 p2 -> Type
IsEquiv (PathSquare_ind P)
  srapply isequiv_adjointify.H: Funext
A: Type
P: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01)
(p2 : a10 = a11), PathSquare p p0 p1 p2 -> Type
(forall (a00 a10 a01 a11 : A) (p : a00 = a10)
 (p0 : a01 = a11) (p1 : a00 = a01) (p2 : a10 = a11)
 (p3 : PathSquare p p0 p1 p2),
 P a00 a10 a01 a11 p p0 p1 p2 p3) ->
forall x : A, P x x x x 1 1 1 1 1%square
H: Funext
A: Type
P: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01)
(p2 : a10 = a11), PathSquare p p0 p1 p2 -> Type
PathSquare_ind P o ?g == idmap
H: Funext
A: Type
P: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01)
(p2 : a10 = a11), PathSquare p p0 p1 p2 -> Type
?g o PathSquare_ind P == idmap
  1: intros X ?; apply X.H: Funext
A: Type
P: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01)
(p2 : a10 = a11), PathSquare p p0 p1 p2 -> Type
PathSquare_ind P
o (fun
     (X : forall (a00 a10 a01 a11 : A) (p : a00 = a10)
          (p0 : a01 = a11) (p1 : a00 = a01)
          (p2 : a10 = a11)
          (p3 : PathSquare p p0 p1 p2),
          P a00 a10 a01 a11 p p0 p1 p2 p3) (x : A) =>
   X x x x x 1 1 1 1 1%square) == idmap
H: Funext
A: Type
P: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01)
(p2 : a10 = a11), PathSquare p p0 p1 p2 -> Type
(fun
   (X : forall (a00 a10 a01 a11 : A) (p : a00 = a10)
        (p0 : a01 = a11) (p1 : a00 = a01)
        (p2 : a10 = a11) (p3 : PathSquare p p0 p1 p2),
        P a00 a10 a01 a11 p p0 p1 p2 p3) (x : A) =>
 X x x x x 1 1 1 1 1%square) o PathSquare_ind P ==
idmap
  2: intro; reflexivity.H: Funext
A: Type
P: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01)
(p2 : a10 = a11), PathSquare p p0 p1 p2 -> Type
PathSquare_ind P
o (fun
     (X : forall (a00 a10 a01 a11 : A) (p : a00 = a10)
          (p0 : a01 = a11) (p1 : a00 = a01)
          (p2 : a10 = a11)
          (p3 : PathSquare p p0 p1 p2),
          P a00 a10 a01 a11 p p0 p1 p2 p3) (x : A) =>
   X x x x x 1 1 1 1 1%square) == idmap
  intro.H: Funext
A: Type
P: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01)
(p2 : a10 = a11), PathSquare p p0 p1 p2 -> Type
x: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01) (p2 : a10 = a11)
(p3 : PathSquare p p0 p1 p2),
P a00 a10 a01 a11 p p0 p1 p2 p3
@PathSquare_ind A P
  (fun x0 : A => x x0 x0 x0 x0 1 1 1 1 1%square) = x
  do 8 (apply path_forall; intro).H: Funext
A: Type
P: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01)
(p2 : a10 = a11), PathSquare p p0 p1 p2 -> Type
x: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01) (p2 : a10 = a11)
(p3 : PathSquare p p0 p1 p2),
P a00 a10 a01 a11 p p0 p1 p2 p3
x0, x1, x2, x3: A
x4: x0 = x1
x5: x2 = x3
x6: x0 = x2
x7: x1 = x3
PathSquare_ind P
  (fun x0 : A => x x0 x0 x0 x0 1 1 1 1 1%square) =
x x0 x1 x2 x3 x4 x5 x6 x7
  apply path_forall.H: Funext
A: Type
P: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01)
(p2 : a10 = a11), PathSquare p p0 p1 p2 -> Type
x: forall (a00 a10 a01 a11 : A) (p : a00 = a10)
(p0 : a01 = a11) (p1 : a00 = a01) (p2 : a10 = a11)
(p3 : PathSquare p p0 p1 p2),
P a00 a10 a01 a11 p p0 p1 p2 p3
x0, x1, x2, x3: A
x4: x0 = x1
x5: x2 = x3
x6: x0 = x2
x7: x1 = x3
PathSquare_ind P
  (fun x0 : A => x x0 x0 x0 x0 1 1 1 1 1%square) ==
x x0 x1 x2 x3 x4 x5 x6 x7
  by intros [].
Defined.

(** [PathSquare]s can be given by 2-dimensional paths. *)
Definition equiv_sq_path {A} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11}
  {p0x : a00 = a01} {p1x : a10 = a11}
  : px0 @ p1x = p0x @ px1 <~> PathSquare px0 px1 p0x p1x.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px0 @ p1x = p0x @ px1 <~> PathSquare px0 px1 p0x p1x
Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px0 @ p1x = p0x @ px1 <~> PathSquare px0 px1 p0x p1x
  snapply Build_Equiv.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px0 @ p1x = p0x @ px1 -> PathSquare px0 px1 p0x p1x
A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
IsEquiv ?equiv_fun
  {A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px0 @ p1x = p0x @ px1 -> PathSquare px0 px1 p0x p1x destruct p0x, p1x.A: Type
a00, a10: A
px0, px1: a00 = a10
px0 @ 1 = 1 @ px1 -> PathSquare px0 px1 1 1
    intro e.A: Type
a00, a10: A
px0, px1: a00 = a10
e: px0 @ 1 = 1 @ px1
PathSquare px0 px1 1 1
    generalize (e @ concat_1p _).A: Type
a00, a10: A
px0, px1: a00 = a10
e: px0 @ 1 = 1 @ px1
px0 @ 1 = px1 -> PathSquare px0 px1 1 1
    intro e'.A: Type
a00, a10: A
px0, px1: a00 = a10
e: px0 @ 1 = 1 @ px1
e': px0 @ 1 = px1
PathSquare px0 px1 1 1
    destruct e', px0.A: Type
a00: A
e: 1 @ 1 = 1 @ (1 @ 1)
PathSquare 1 (1 @ 1) 1 1
    exact sq_id. }A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
IsEquiv
  (match
     p0x as p in (_ = a)
     return
       (forall px1 : a = a11,
        px0 @ p1x = p @ px1 ->
        PathSquare px0 px1 p p1x)
   with
   | 1 =>
       fun px1 : a00 = a11 =>
       match
         p1x as p in (_ = a)
         return
           (forall px2 : a00 = a,
            px0 @ p = 1 @ px2 ->
            PathSquare px0 px2 1 p)
       with
       | 1 =>
           fun (px2 : a00 = a10)
             (e : px0 @ 1 = 1 @ px2) =>
           (fun e' : px0 @ 1 = px2 =>
            match
              e' in (_ = p)
              return
                (px0 @ 1 = 1 @ p ->
                 PathSquare px0 p 1 1)
            with
            | 1 =>
                fun e0 : px0 @ 1 = 1 @ (px0 @ 1) =>
                match
                  px0 as p in (_ = a)
                  return
                    (p @ 1 = 1 @ (...) ->
                     PathSquare p (p @ 1) 1 1)
                with
                | 1 =>
                    fun _ : 1 @ 1 = 1 @ (1 @ 1) =>
                    1%square
                end e0
            end e) (e @ concat_1p px2)
       end px1
   end px1)
  srapply isequiv_adjointify; try by intros [].A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
(fun X : PathSquare px0 px1 p0x p1x =>
 match
   X in (@PathSquare _ a00 a10 a01 a11 p p0 p1 p2)
   return (p @ p2 = p1 @ p0)
 with
 | @sq_id _ x => (fun x0 : A => 1) x
 end)
o match
    p0x as p in (_ = a)
    return
      (forall px1 : a = a11,
       px0 @ p1x = p @ px1 -> PathSquare px0 px1 p p1x)
  with
  | 1 =>
      fun px1 : a00 = a11 =>
      match
        p1x as p in (_ = a)
        return
          (forall px2 : a00 = a,
           px0 @ p = 1 @ px2 -> PathSquare px0 px2 1 p)
      with
      | 1 =>
          fun (px2 : a00 = a10)
            (e : px0 @ 1 = 1 @ px2) =>
          (fun e' : px0 @ 1 = px2 =>
           match
             e' in (_ = p)
             return
               (px0 @ 1 = 1 @ p ->
                PathSquare px0 p 1 1)
           with
           | 1 =>
               fun e0 : px0 @ 1 = 1 @ (px0 @ 1) =>
               match
                 px0 as p in (_ = a)
                 return
                   (p @ 1 = 1 @ (...) ->
                    PathSquare p (p @ 1) 1 1)
               with
               | 1 =>
                   fun _ : 1 @ 1 = 1 @ (1 @ 1) =>
                   1%square
               end e0
           end e) (e @ concat_1p px2)
      end px1
  end px1 == idmap
  destruct p0x, p1x.A: Type
a00, a10: A
px0, px1: a00 = a10
(fun x : px0 @ 1 = 1 @ px1 =>
 match
   match
     x @ concat_1p px1 in (_ = p)
     return (px0 @ 1 = 1 @ p -> PathSquare px0 p 1 1)
   with
   | 1 =>
       fun e : px0 @ 1 = 1 @ (px0 @ 1) =>
       match
         px0 as p in (_ = a)
         return
           (p @ 1 = 1 @ (p @ 1) ->
            PathSquare p (p @ 1) 1 1)
       with
       | 1 => fun _ : 1 @ 1 = 1 @ (1 @ 1) => 1%square
       end e
   end x in (@PathSquare _ a00 a10 a01 a11 p p0 p1 p2)
   return (p @ p2 = p1 @ p0)
 with
 | @sq_id _ x0 => 1
 end) == idmap
  intros e.A: Type
a00, a10: A
px0, px1: a00 = a10
e: px0 @ 1 = 1 @ px1
match
  match
    e @ concat_1p px1 in (_ = p)
    return (px0 @ 1 = 1 @ p -> PathSquare px0 p 1 1)
  with
  | 1 =>
      fun e : px0 @ 1 = 1 @ (px0 @ 1) =>
      match
        px0 as p in (_ = a)
        return
          (p @ 1 = 1 @ (p @ 1) ->
           PathSquare p (p @ 1) 1 1)
      with
      | 1 => fun _ : 1 @ 1 = 1 @ (1 @ 1) => 1%square
      end e
  end e in (@PathSquare _ a00 a10 a01 a11 p p0 p1 p2)
  return (p @ p2 = p1 @ p0)
with
| @sq_id _ x => 1
end = e
  pattern e.A: Type
a00, a10: A
px0, px1: a00 = a10
e: px0 @ 1 = 1 @ px1
(fun p : px0 @ 1 = 1 @ px1 =>
 match
   match
     p @ concat_1p px1 in (_ = p0)
     return
       (px0 @ 1 = 1 @ p0 -> PathSquare px0 p0 1 1)
   with
   | 1 =>
       fun e : px0 @ 1 = 1 @ (px0 @ 1) =>
       match
         px0 as p0 in (_ = a)
         return
           (p0 @ 1 = 1 @ (p0 @ 1) ->
            PathSquare p0 (p0 @ 1) 1 1)
       with
       | 1 => fun _ : 1 @ 1 = 1 @ (1 @ 1) => 1%square
       end e
   end p in
   (@PathSquare _ a00 a10 a01 a11 p0 p1 p2 p3)
   return (p0 @ p3 = p2 @ p1)
 with
 | @sq_id _ x => 1
 end = p) e
  pose (e' := e @ concat_1p _).A: Type
a00, a10: A
px0, px1: a00 = a10
e: px0 @ 1 = 1 @ px1
e':= e @ concat_1p px1: px0 @ 1 = px1
(fun p : px0 @ 1 = 1 @ px1 =>
 match
   match
     p @ concat_1p px1 in (_ = p0)
     return
       (px0 @ 1 = 1 @ p0 -> PathSquare px0 p0 1 1)
   with
   | 1 =>
       fun e : px0 @ 1 = 1 @ (px0 @ 1) =>
       match
         px0 as p0 in (_ = a)
         return
           (p0 @ 1 = 1 @ (p0 @ 1) ->
            PathSquare p0 (p0 @ 1) 1 1)
       with
       | 1 => fun _ : 1 @ 1 = 1 @ (1 @ 1) => 1%square
       end e
   end p in
   (@PathSquare _ a00 a10 a01 a11 p0 p1 p2 p3)
   return (p0 @ p3 = p2 @ p1)
 with
 | @sq_id _ x => 1
 end = p) e
  pose (e'' := e' @ (concat_1p _)^).A: Type
a00, a10: A
px0, px1: a00 = a10
e: px0 @ 1 = 1 @ px1
e':= e @ concat_1p px1: px0 @ 1 = px1
e'':= e' @ (concat_1p px1)^: px0 @ 1 = 1 @ px1
(fun p : px0 @ 1 = 1 @ px1 =>
 match
   match
     p @ concat_1p px1 in (_ = p0)
     return
       (px0 @ 1 = 1 @ p0 -> PathSquare px0 p0 1 1)
   with
   | 1 =>
       fun e : px0 @ 1 = 1 @ (px0 @ 1) =>
       match
         px0 as p0 in (_ = a)
         return
           (p0 @ 1 = 1 @ (p0 @ 1) ->
            PathSquare p0 (p0 @ 1) 1 1)
       with
       | 1 => fun _ : 1 @ 1 = 1 @ (1 @ 1) => 1%square
       end e
   end p in
   (@PathSquare _ a00 a10 a01 a11 p0 p1 p2 p3)
   return (p0 @ p3 = p2 @ p1)
 with
 | @sq_id _ x => 1
 end = p) e
  refine (@transport _ _ e'' e _ _).A: Type
a00, a10: A
px0, px1: a00 = a10
e: px0 @ 1 = 1 @ px1
e':= e @ concat_1p px1: px0 @ 1 = px1
e'':= e' @ (concat_1p px1)^: px0 @ 1 = 1 @ px1
e'' = e
A: Type
a00, a10: A
px0, px1: a00 = a10
e: px0 @ 1 = 1 @ px1
e':= e @ concat_1p px1: px0 @ 1 = px1
e'':= e' @ (concat_1p px1)^: px0 @ 1 = 1 @ px1
match
  match
    e'' @ concat_1p px1 in (_ = p)
    return (px0 @ 1 = 1 @ p -> PathSquare px0 p 1 1)
  with
  | 1 =>
      fun e : px0 @ 1 = 1 @ (px0 @ 1) =>
      match
        px0 as p in (_ = a)
        return
          (p @ 1 = 1 @ (p @ 1) ->
           PathSquare p (p @ 1) 1 1)
      with
      | 1 => fun _ : 1 @ 1 = 1 @ (1 @ 1) => 1%square
      end e
  end e'' in
  (@PathSquare _ a00 a10 a01 a11 p p0 p1 p2)
  return (p @ p2 = p1 @ p0)
with
| @sq_id _ x => 1
end = e''
  -A: Type
a00, a10: A
px0, px1: a00 = a10
e: px0 @ 1 = 1 @ px1
e':= e @ concat_1p px1: px0 @ 1 = px1
e'':= e' @ (concat_1p px1)^: px0 @ 1 = 1 @ px1
e'' = e subst e' e''; hott_simpl.
  -A: Type
a00, a10: A
px0, px1: a00 = a10
e: px0 @ 1 = 1 @ px1
e':= e @ concat_1p px1: px0 @ 1 = px1
e'':= e' @ (concat_1p px1)^: px0 @ 1 = 1 @ px1
match
  match
    e'' @ concat_1p px1 in (_ = p)
    return (px0 @ 1 = 1 @ p -> PathSquare px0 p 1 1)
  with
  | 1 =>
      fun e : px0 @ 1 = 1 @ (px0 @ 1) =>
      match
        px0 as p in (_ = a)
        return
          (p @ 1 = 1 @ (p @ 1) ->
           PathSquare p (p @ 1) 1 1)
      with
      | 1 => fun _ : 1 @ 1 = 1 @ (1 @ 1) => 1%square
      end e
  end e'' in
  (@PathSquare _ a00 a10 a01 a11 p p0 p1 p2)
  return (p @ p2 = p1 @ p0)
with
| @sq_id _ x => 1
end = e'' clearbody e'; clear e.A: Type
a00, a10: A
px0, px1: a00 = a10
e': px0 @ 1 = px1
e'':= e' @ (concat_1p px1)^: px0 @ 1 = 1 @ px1
match
  match
    e'' @ concat_1p px1 in (_ = p)
    return (px0 @ 1 = 1 @ p -> PathSquare px0 p 1 1)
  with
  | 1 =>
      fun e : px0 @ 1 = 1 @ (px0 @ 1) =>
      match
        px0 as p in (_ = a)
        return
          (p @ 1 = 1 @ (p @ 1) ->
           PathSquare p (p @ 1) 1 1)
      with
      | 1 => fun _ : 1 @ 1 = 1 @ (1 @ 1) => 1%square
      end e
  end e'' in
  (@PathSquare _ a00 a10 a01 a11 p p0 p1 p2)
  return (p @ p2 = p1 @ p0)
with
| @sq_id _ x => 1
end = e''
    destruct e', px0.A: Type
a00: A
e'':= 1 @ (concat_1p (1 @ 1))^: 1 @ 1 = 1 @ (1 @ 1)
match
  match
    e'' @ concat_1p (1 @ 1) in (_ = p)
    return (1 @ 1 = 1 @ p -> PathSquare 1 p 1 1)
  with
  | 1 => fun _ : 1 @ 1 = 1 @ (1 @ 1) => 1%square
  end e'' in
  (@PathSquare _ a00 a10 a01 a11 p p0 p1 p2)
  return (p @ p2 = p1 @ p0)
with
| @sq_id _ x => 1
end = e''
    reflexivity.
Defined.

Notation sq_path := equiv_sq_path.

(** Squares in (n+2)-truncated types are n-truncated. *)
Instance istrunc_sq n
  {A} `{!IsTrunc n.+2 A} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11}
  {p0x : a00 = a01} {p1x : a10 = a11}
  : IsTrunc n (PathSquare px0 px1 p0x p1x).n: trunc_index
A: Type
IsTrunc0: IsTrunc n.+2 A
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
IsTrunc n (PathSquare px0 px1 p0x p1x)
Proof.n: trunc_index
A: Type
IsTrunc0: IsTrunc n.+2 A
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
IsTrunc n (PathSquare px0 px1 p0x p1x)
  exact (istrunc_equiv_istrunc _ sq_path).
Defined.

(** We can give degenerate squares. *)
Section PathSquaresFromPaths.

  Context
    {A : Type} {a00 a10 a01 : A}
    {p p' : a00 = a10} {q q' : a00 = a01}.

  Definition equiv_sq_G1  : p = p' <~> PathSquare p p' 1 1
    := sq_path oE equiv_p1_1q.

  Definition equiv_sq_1G : q = q' <~> PathSquare 1 1 q q'
    := sq_path oE equiv_1p_q1 oE equiv_path_inverse _ _.

End PathSquaresFromPaths.

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. *)
Definition sq_refl_h {A} {a0 a1 : A} (p : a0 = a1)
  : PathSquare p p 1 1 := sq_G1 1.

(** [PathSquare] vertical reflexivity. *)
Definition sq_refl_v {A} {a0 a1 : A} (p : a0 = a1)
  : PathSquare 1 1 p p := sq_1G 1.

(** Horizontal flip. *)
Definition equiv_sq_flip_h {A : Type} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
  : PathSquare px0 px1 p0x p1x <~> PathSquare px1 px0 p0x^ p1x^.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
PathSquare px1 px0 p0x^ p1x^
Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
PathSquare px1 px0 p0x^ p1x^
  destruct p0x, p1x.A: Type
a00, a10: A
px0, px1: a00 = a10
PathSquare px0 px1 1 1 <~> PathSquare px1 px0 1^ 1^
  refine (sq_G1 oE _).A: Type
a00, a10: A
px0, px1: a00 = a10
PathSquare px0 px1 1 1 <~> px1 = px0
  refine (equiv_path_inverse _ _ oE _).A: Type
a00, a10: A
px0, px1: a00 = a10
PathSquare px0 px1 1 1 <~> px0 = px1
  exact sq_G1^-1.
Defined.

Notation sq_flip_h := equiv_sq_flip_h.

(** Vertical flip. *)
Definition equiv_sq_flip_v {A : Type} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
  : PathSquare px0 px1 p0x p1x <~> PathSquare px0^ px1^ p1x p0x.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
PathSquare px0^ px1^ p1x p0x
Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
PathSquare px0^ px1^ p1x p0x
  destruct px0, px1.A: Type
a00, a01: A
p0x, p1x: a00 = a01
PathSquare 1 1 p0x p1x <~> PathSquare 1^ 1^ p1x p0x
  refine (sq_1G oE _).A: Type
a00, a01: A
p0x, p1x: a00 = a01
PathSquare 1 1 p0x p1x <~> p1x = p0x
  refine (equiv_path_inverse _ _ oE _).A: Type
a00, a01: A
p0x, p1x: a00 = a01
PathSquare 1 1 p0x p1x <~> p0x = p1x
  exact sq_1G^-1.
Defined.

Notation sq_flip_v := equiv_sq_flip_v.

(** Transpose of a square. We make a local definition that will never get unfolded. *)
Local Definition tr {A : Type} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
  : PathSquare px0 px1 p0x p1x -> PathSquare p0x p1x px0 px1.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x ->
PathSquare p0x p1x px0 px1
Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x ->
PathSquare p0x p1x px0 px1
  by intros [].
Defined.

Arguments tr : simpl never.

Definition equiv_sq_tr {A : Type} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
  : PathSquare px0 px1 p0x p1x <~> PathSquare p0x p1x px0 px1.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
PathSquare p0x p1x px0 px1
Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
PathSquare p0x p1x px0 px1
  srapply (equiv_adjointify tr tr).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
tr o tr == idmap
A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
tr o tr == idmap
  1,2: by intros [].
Defined.

Notation sq_tr := equiv_sq_tr.

(** NOTE: sq_tr ought to be some sort of involution but it obviously isn't since it is not of the form A -> A. Perhaps there is a more general "involution" but between equivalent types? But then that very equivalence is given by sq_tr so it seems a bit circular... *)

Definition sq_tr_refl_h {A} {a b : A} {p : a = b}
  : sq_tr (sq_refl_h p) = sq_refl_v p.A: Type
a, b: A
p: a = b
sq_tr (sq_refl_h p) = sq_refl_v p
Proof.A: Type
a, b: A
p: a = b
sq_tr (sq_refl_h p) = sq_refl_v p
  by destruct p.
Defined.

Definition sq_tr_refl_v {A} {a b : A} {p : a = b}
  : sq_tr (sq_refl_v p) = sq_refl_h p.A: Type
a, b: A
p: a = b
sq_tr (sq_refl_v p) = sq_refl_h p
Proof.A: Type
a, b: A
p: a = b
sq_tr (sq_refl_v p) = sq_refl_h p
  by destruct p.
Defined.

(** Operations on squares. *)
Section PathSquareOps.

  Context
    {A : Type}
    {a00 a10 a01 a11 : A}
    {px0 : a00 = a10} {px1 : a01 = a11}
    {p0x : a00 = a01} {p1x : a10 = a11}.

  (** Inverse square. *)
  Definition equiv_sq_V : PathSquare px0 px1 p0x p1x <~> PathSquare px1^ px0^ p1x^ p0x^.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
PathSquare px1^ px0^ p1x^ p0x^
  Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
PathSquare px1^ px0^ p1x^ p0x^
    refine (sq_path oE _ ).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
px1^ @ p0x^ = p1x^ @ px0^
    refine (equiv_concat_lr (inv_pp _ _)^ (inv_pp _ _) oE _).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
(p0x @ px1)^ = (px0 @ p1x)^
    refine (equiv_ap _ _ _ oE _).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~> p0x @ px1 = px0 @ p1x
    refine (sq_path^-1 oE _).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
PathSquare p0x p1x px0 px1
    exact sq_tr.
  Defined.

  (** Left rotation : left right top bottom  ->  top bottom right left. *)
  Definition equiv_sq_rot_l : PathSquare px0 px1 p0x p1x <~> PathSquare p0x^ p1x^ px1 px0.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
PathSquare p0x^ p1x^ px1 px0
  Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
PathSquare p0x^ p1x^ px1 px0
    refine (sq_path oE _).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~> p0x^ @ px0 = px1 @ p1x^
    refine (equiv_moveR_Vp _ _ _ oE _).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
px0 = p0x @ (px1 @ p1x^)
    refine (equiv_concat_r (concat_pp_p _ _ _) _ oE _).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
px0 = (p0x @ px1) @ p1x^
    refine (equiv_moveL_pV _ _ _ oE _).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~> px0 @ p1x = p0x @ px1
    exact sq_path^-1.
  Defined.

  (** Right rotation : left right top bottom -> bottom top left right. *)
  Definition equiv_sq_rot_r : PathSquare px0 px1 p0x p1x -> PathSquare p1x p0x px0^ px1^.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x ->
PathSquare p1x p0x px0^ px1^
  Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x ->
PathSquare p1x p0x px0^ px1^
    refine (sq_path oE _).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~> p1x @ px1^ = px0^ @ p0x
    refine (equiv_moveL_Vp _ _ _ oE _).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
px0 @ (p1x @ px1^) = p0x
    refine (equiv_concat_l (concat_p_pp _ _ _) _ oE _).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~>
(px0 @ p1x) @ px1^ = p0x
    refine (equiv_moveR_pV _ _ _ oE _).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x <~> px0 @ p1x = p0x @ px1
    exact sq_path^-1.
  Defined.

End PathSquareOps.

Notation sq_V := equiv_sq_V.
Notation sq_rot_l:= equiv_sq_rot_l.
Notation sq_rot_r := equiv_sq_rot_r.

(** Lemmas for rewriting sides of squares. *)
Section PathSquareRewriting.

  Context {A : Type}
    {a00 a10 a01 a11 : A}
    {px0 : a00 = a10} {px1 : a01 = a11}
    {p0x : a00 = a01} {p1x : a10 = a11}.

  (** These are all special cases of the following "rewrite all sides" lemma which we prove is an equivalence giving us all special cases as equivalences too. *)

  Definition equiv_sq_GGGG {px0' px1' p0x' p1x'} (qx0 : px0 = px0')
    (qx1 : px1 = px1') (q0x : p0x = p0x') (q1x : p1x = p1x')
    : PathSquare px0 px1 p0x p1x <~> PathSquare px0' px1' p0x' p1x'.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px0': a00 = a10
px1': a01 = a11
p0x': a00 = a01
p1x': a10 = a11
qx0: px0 = px0'
qx1: px1 = px1'
q0x: p0x = p0x'
q1x: p1x = p1x'
PathSquare px0 px1 p0x p1x <~>
PathSquare px0' px1' p0x' p1x'
  Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px0': a00 = a10
px1': a01 = a11
p0x': a00 = a01
p1x': a10 = a11
qx0: px0 = px0'
qx1: px1 = px1'
q0x: p0x = p0x'
q1x: p1x = p1x'
PathSquare px0 px1 p0x p1x <~>
PathSquare px0' px1' p0x' p1x'
    by destruct qx0, qx1, q0x, q1x.
  Defined.

  Context {px0' px1' p0x' p1x'}
    (qx0 : px0 = px0') (qx1 : px1 = px1')
    (q0x : p0x = p0x') (q1x : p1x = p1x').

  Definition equiv_sq_Gccc := equiv_sq_GGGG qx0 1 1 1.
  Definition equiv_sq_cGcc := equiv_sq_GGGG 1 qx1 1 1.
  Definition equiv_sq_ccGc := equiv_sq_GGGG 1 1 q0x 1.
  Definition equiv_sq_cccG := equiv_sq_GGGG 1 1 1 q1x.
  Definition equiv_sq_GGcc := equiv_sq_GGGG qx0 qx1 1 1.
  Definition equiv_sq_GcGc := equiv_sq_GGGG qx0 1 q0x 1.
  Definition equiv_sq_GccG := equiv_sq_GGGG qx0 1 1 q1x.
  Definition equiv_sq_cGGc := equiv_sq_GGGG 1 qx1 q0x 1.
  Definition equiv_sq_cGcG := equiv_sq_GGGG 1 qx1 1 q1x.
  Definition equiv_sq_ccGG := equiv_sq_GGGG 1 1 q0x q1x.
  Definition equiv_sq_GGGc := equiv_sq_GGGG qx0 qx1 q0x 1.
  Definition equiv_sq_cGGG := equiv_sq_GGGG 1 qx1 q0x q1x.

End PathSquareRewriting.

Notation sq_GGGG := equiv_sq_GGGG.
Notation sq_Gccc := equiv_sq_Gccc.
Notation sq_cGcc := equiv_sq_cGcc.
Notation sq_ccGc := equiv_sq_ccGc.
Notation sq_cccG := equiv_sq_cccG.
Notation sq_GGcc := equiv_sq_GGcc.
Notation sq_GcGc := equiv_sq_GcGc.
Notation sq_GccG := equiv_sq_GccG.
Notation sq_cGGc := equiv_sq_cGGc.
Notation sq_cGcG := equiv_sq_cGcG.
Notation sq_ccGG := equiv_sq_ccGG.
Notation sq_GGGc := equiv_sq_GGGc.
Notation sq_cGGG := equiv_sq_cGGG.

Section MovePaths.
  Context {A : Type} {x x00 x20 x02 x22 : A}
  {f10 : x00 = x20} {f12 : x02 = x22} {f01 : x00 = x02} {f21 : x20 = x22}.
  (** Operations to move paths around a square. We define all these operations immediately as equivalences. The naming first number indicates in which argument the path that moves is on the left of the equivalence, and the second number where it is on the right. The equivalences are all set up so that on the right, there is no path inversion. For the [24] and [13] equivalences there is a path inverse on the left. The corresponding equivalences [42] and [31] are the symmetric versions of these, but the path inverse is in another place. *)

  Definition equiv_sq_move_23 {f12'' : x02 = x} {f12' : x = x22} 
    : PathSquare f10 (f12'' @ f12') f01 f21 <~> PathSquare f10 f12' (f01 @ f12'') f21.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f12'': x02 = x
f12': x = x22
PathSquare f10 (f12'' @ f12') f01 f21 <~>
PathSquare f10 f12' (f01 @ f12'') f21
  Proof.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f12'': x02 = x
f12': x = x22
PathSquare f10 (f12'' @ f12') f01 f21 <~>
PathSquare f10 f12' (f01 @ f12'') f21
    clear f12.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f01: x00 = x02
f21: x20 = x22
f12'': x02 = x
f12': x = x22
PathSquare f10 (f12'' @ f12') f01 f21 <~>
PathSquare f10 f12' (f01 @ f12'') f21 destruct f12''.A: Type
x00, x20, x02, x22: A
f10: x00 = x20
f01: x00 = x02
f21: x20 = x22
f12': x02 = x22
PathSquare f10 (1 @ f12') f01 f21 <~>
PathSquare f10 f12' (f01 @ 1) f21
    refine (sq_cGcc (concat_1p _) oE _).A: Type
x00, x20, x02, x22: A
f10: x00 = x20
f01: x00 = x02
f21: x20 = x22
f12': x02 = x22
PathSquare f10 (1 @ f12') f01 f21 <~>
PathSquare f10 (1 @ f12') (f01 @ 1) f21
    exact (sq_ccGc (concat_p1 _)^).
  Defined.

  Definition equiv_sq_move_14 {f10'' : x00 = x} {f10' : x = x20} 
    : PathSquare (f10'' @ f10') f12 f01 f21 <~> PathSquare f10'' f12 f01 (f10' @ f21).A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f10'': x00 = x
f10': x = x20
PathSquare (f10'' @ f10') f12 f01 f21 <~>
PathSquare f10'' f12 f01 (f10' @ f21)
  Proof.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f10'': x00 = x
f10': x = x20
PathSquare (f10'' @ f10') f12 f01 f21 <~>
PathSquare f10'' f12 f01 (f10' @ f21)
    clear f10.A: Type
x, x00, x20, x02, x22: A
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f10'': x00 = x
f10': x = x20
PathSquare (f10'' @ f10') f12 f01 f21 <~>
PathSquare f10'' f12 f01 (f10' @ f21) destruct f10'.A: Type
x, x00, x02, x22: A
f12: x02 = x22
f01: x00 = x02
f21: x = x22
f10'': x00 = x
PathSquare (f10'' @ 1) f12 f01 f21 <~>
PathSquare f10'' f12 f01 (1 @ f21)
    refine (sq_cccG (concat_1p _)^ oE _).A: Type
x, x00, x02, x22: A
f12: x02 = x22
f01: x00 = x02
f21: x = x22
f10'': x00 = x
PathSquare (f10'' @ 1) f12 f01 f21 <~>
PathSquare f10'' f12 f01 f21
    exact (sq_Gccc (concat_p1 _)).
  Defined.

  Definition equiv_sq_move_24 {f12'' : x02 = x} {f12' : x22 = x} 
    : PathSquare f10 (f12'' @ f12'^) f01 f21 <~> PathSquare f10 f12'' f01 (f21 @ f12').A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f12'': x02 = x
f12': x22 = x
PathSquare f10 (f12'' @ f12'^) f01 f21 <~>
PathSquare f10 f12'' f01 (f21 @ f12')
  Proof.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f12'': x02 = x
f12': x22 = x
PathSquare f10 (f12'' @ f12'^) f01 f21 <~>
PathSquare f10 f12'' f01 (f21 @ f12')
    clear f12.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f01: x00 = x02
f21: x20 = x22
f12'': x02 = x
f12': x22 = x
PathSquare f10 (f12'' @ f12'^) f01 f21 <~>
PathSquare f10 f12'' f01 (f21 @ f12') destruct f12'.A: Type
x00, x20, x02, x22: A
f10: x00 = x20
f01: x00 = x02
f21: x20 = x22
f12'': x02 = x22
PathSquare f10 (f12'' @ 1^) f01 f21 <~>
PathSquare f10 f12'' f01 (f21 @ 1)
    refine (sq_cccG (concat_p1 _)^ oE _).A: Type
x00, x20, x02, x22: A
f10: x00 = x20
f01: x00 = x02
f21: x20 = x22
f12'': x02 = x22
PathSquare f10 (f12'' @ 1^) f01 f21 <~>
PathSquare f10 f12'' f01 f21
    exact (sq_cGcc (concat_p1 _)).
  Defined.

  Definition equiv_sq_move_42 {f12'' : x02 = x} {f12' : x = x22} 
    : PathSquare f10 f12'' f01 (f21 @ f12'^) <~> PathSquare f10 (f12'' @ f12') f01 f21.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f12'': x02 = x
f12': x = x22
PathSquare f10 f12'' f01 (f21 @ f12'^) <~>
PathSquare f10 (f12'' @ f12') f01 f21
  Proof.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f12'': x02 = x
f12': x = x22
PathSquare f10 f12'' f01 (f21 @ f12'^) <~>
PathSquare f10 (f12'' @ f12') f01 f21
    clear f12.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f01: x00 = x02
f21: x20 = x22
f12'': x02 = x
f12': x = x22
PathSquare f10 f12'' f01 (f21 @ f12'^) <~>
PathSquare f10 (f12'' @ f12') f01 f21 destruct f12'.A: Type
x, x00, x20, x02: A
f10: x00 = x20
f01: x00 = x02
f21: x20 = x
f12'': x02 = x
PathSquare f10 f12'' f01 (f21 @ 1^) <~>
PathSquare f10 (f12'' @ 1) f01 f21
    refine (sq_cGcc (concat_p1 _)^ oE _).A: Type
x, x00, x20, x02: A
f10: x00 = x20
f01: x00 = x02
f21: x20 = x
f12'': x02 = x
PathSquare f10 f12'' f01 (f21 @ 1^) <~>
PathSquare f10 f12'' f01 f21
    exact (sq_cccG (concat_p1 _)).
  Defined.

  Definition equiv_sq_move_13 {f10'' : x = x00} {f10' : x = x20} 
    : PathSquare (f10''^ @ f10') f12 f01 f21 <~> PathSquare f10' f12 (f10'' @ f01) f21.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f10'': x = x00
f10': x = x20
PathSquare (f10''^ @ f10') f12 f01 f21 <~>
PathSquare f10' f12 (f10'' @ f01) f21
  Proof.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f10'': x = x00
f10': x = x20
PathSquare (f10''^ @ f10') f12 f01 f21 <~>
PathSquare f10' f12 (f10'' @ f01) f21
    clear f10.A: Type
x, x00, x20, x02, x22: A
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f10'': x = x00
f10': x = x20
PathSquare (f10''^ @ f10') f12 f01 f21 <~>
PathSquare f10' f12 (f10'' @ f01) f21 destruct f10''.A: Type
x, x20, x02, x22: A
f12: x02 = x22
f01: x = x02
f21: x20 = x22
f10': x = x20
PathSquare (1^ @ f10') f12 f01 f21 <~>
PathSquare f10' f12 (1 @ f01) f21
    refine (sq_ccGc (concat_1p _)^ oE _).A: Type
x, x20, x02, x22: A
f12: x02 = x22
f01: x = x02
f21: x20 = x22
f10': x = x20
PathSquare (1^ @ f10') f12 f01 f21 <~>
PathSquare f10' f12 f01 f21
    exact (sq_Gccc (concat_1p _)).
  Defined.

  Definition equiv_sq_move_31 {f10'' : x00 = x} {f10' : x = x20} 
    : PathSquare f10' f12 (f10''^ @ f01) f21 <~> PathSquare (f10'' @ f10') f12 f01 f21.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f10'': x00 = x
f10': x = x20
PathSquare f10' f12 (f10''^ @ f01) f21 <~>
PathSquare (f10'' @ f10') f12 f01 f21
  Proof.A: Type
x, x00, x20, x02, x22: A
f10: x00 = x20
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f10'': x00 = x
f10': x = x20
PathSquare f10' f12 (f10''^ @ f01) f21 <~>
PathSquare (f10'' @ f10') f12 f01 f21
    clear f10.A: Type
x, x00, x20, x02, x22: A
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f10'': x00 = x
f10': x = x20
PathSquare f10' f12 (f10''^ @ f01) f21 <~>
PathSquare (f10'' @ f10') f12 f01 f21 destruct f10''.A: Type
x00, x20, x02, x22: A
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f10': x00 = x20
PathSquare f10' f12 (1^ @ f01) f21 <~>
PathSquare (1 @ f10') f12 f01 f21
    refine (sq_Gccc (concat_1p _)^ oE _).A: Type
x00, x20, x02, x22: A
f12: x02 = x22
f01: x00 = x02
f21: x20 = x22
f10': x00 = x20
PathSquare f10' f12 (1^ @ f01) f21 <~>
PathSquare f10' f12 f01 f21
    exact (sq_ccGc (concat_1p _)).
  Defined.

End MovePaths.

Notation sq_move_23 := equiv_sq_move_23.
Notation sq_move_14 := equiv_sq_move_14.
Notation sq_move_24 := equiv_sq_move_24.
Notation sq_move_42 := equiv_sq_move_42.
Notation sq_move_13 := equiv_sq_move_13.
Notation sq_move_31 := equiv_sq_move_31.

(** Dependent path product definition of [PathSquare]. *)
Definition equiv_sq_dp_prod {A : Type} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
  : DPath (fun xy => fst xy = snd xy) (path_prod' p0x p1x) px0 px1
    <~> PathSquare px0 px1 p0x p1x.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
DPath (fun xy : A * A => fst xy = snd xy)
  (path_prod' p0x p1x) px0 px1 <~>
PathSquare px0 px1 p0x p1x
Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
DPath (fun xy : A * A => fst xy = snd xy)
  (path_prod' p0x p1x) px0 px1 <~>
PathSquare px0 px1 p0x p1x
  refine (_ oE (dp_paths_FlFr _ _ _)^-1).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
((ap fst (path_prod' p0x p1x))^ @ px0) @
ap snd (path_prod' p0x p1x) = px1 <~>
PathSquare px0 px1 p0x p1x
  refine (_ oE (equiv_concat_l (concat_pp_p _ _ _) _)^-1).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
(ap fst (path_prod' p0x p1x))^ @
(px0 @ ap snd (path_prod' p0x p1x)) = px1 <~>
PathSquare px0 px1 p0x p1x
  refine (_ oE equiv_moveL_Mp _ _ _).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px0 @ ap snd (path_prod' p0x p1x) =
ap fst (path_prod' p0x p1x) @ px1 <~>
PathSquare px0 px1 p0x p1x
  refine (_ oE sq_path).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 (ap fst (path_prod' p0x p1x))
  (ap snd (path_prod' p0x p1x)) <~>
PathSquare px0 px1 p0x p1x
  exact (sq_ccGG (ap_fst_path_prod _ _) (ap_snd_path_prod _ _)).
Defined.

Notation sq_dp_prod := equiv_sq_dp_prod.

(** Concatenation of squares. *)
Section PathSquareConcat.

  Context {A : Type} {a00 a10 a01 a11 : A}
    {px0 : a00 = a10} {px1 : a01 = a11}
    {p0x : a00 = a01} {p1x : a10 = a11}.

  (** Horizontal concatenation of squares. *)
  Definition sq_concat_h  {a02 a12 : A}
    {p0y : a01 = a02} {p1y : a11 = a12} {px2 : a02 = a12}
    : PathSquare px0 px1 p0x p1x -> PathSquare px1 px2 p0y p1y
      -> PathSquare px0 px2 (p0x @ p0y) (p1x @ p1y).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
a02, a12: A
p0y: a01 = a02
p1y: a11 = a12
px2: a02 = a12
PathSquare px0 px1 p0x p1x ->
PathSquare px1 px2 p0y p1y ->
PathSquare px0 px2 (p0x @ p0y) (p1x @ p1y)
  Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
a02, a12: A
p0y: a01 = a02
p1y: a11 = a12
px2: a02 = a12
PathSquare px0 px1 p0x p1x ->
PathSquare px1 px2 p0y p1y ->
PathSquare px0 px2 (p0x @ p0y) (p1x @ p1y)
    intros a b.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
a02, a12: A
p0y: a01 = a02
p1y: a11 = a12
px2: a02 = a12
a: PathSquare px0 px1 p0x p1x
b: PathSquare px1 px2 p0y p1y
PathSquare px0 px2 (p0x @ p0y) (p1x @ p1y)
    destruct b.A: Type
a00, a10: A
px0: a00 = a10
x: A
p0x: a00 = x
p1x: a10 = x
a: PathSquare px0 1 p0x p1x
PathSquare px0 1 (p0x @ 1) (p1x @ 1)
    refine (sq_ccGG _ _ a).A: Type
a00, a10: A
px0: a00 = a10
x: A
p0x: a00 = x
p1x: a10 = x
a: PathSquare px0 1 p0x p1x
p0x = p0x @ 1
A: Type
a00, a10: A
px0: a00 = a10
x: A
p0x: a00 = x
p1x: a10 = x
a: PathSquare px0 1 p0x p1x
p1x = p1x @ 1
    1,2: apply inverse, concat_p1.
  Defined.

  (** Vertical concatenation of squares. *)
  Definition sq_concat_v {a20 a21 : A}
    {py0 : a10 = a20} {py1 : a11 = a21} {p2x : a20 = a21}
    : PathSquare px0 px1 p0x p1x -> PathSquare py0 py1 p1x p2x
      -> PathSquare (px0 @ py0) (px1 @ py1) p0x p2x.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
a20, a21: A
py0: a10 = a20
py1: a11 = a21
p2x: a20 = a21
PathSquare px0 px1 p0x p1x ->
PathSquare py0 py1 p1x p2x ->
PathSquare (px0 @ py0) (px1 @ py1) p0x p2x
  Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
a20, a21: A
py0: a10 = a20
py1: a11 = a21
p2x: a20 = a21
PathSquare px0 px1 p0x p1x ->
PathSquare py0 py1 p1x p2x ->
PathSquare (px0 @ py0) (px1 @ py1) p0x p2x
    intros a b.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
a20, a21: A
py0: a10 = a20
py1: a11 = a21
p2x: a20 = a21
a: PathSquare px0 px1 p0x p1x
b: PathSquare py0 py1 p1x p2x
PathSquare (px0 @ py0) (px1 @ py1) p0x p2x
    destruct b.A: Type
a00, a01, x: A
px0: a00 = x
px1: a01 = x
p0x: a00 = a01
a: PathSquare px0 px1 p0x 1
PathSquare (px0 @ 1) (px1 @ 1) p0x 1
    refine (sq_GGcc _ _ a).A: Type
a00, a01, x: A
px0: a00 = x
px1: a01 = x
p0x: a00 = a01
a: PathSquare px0 px1 p0x 1
px0 = px0 @ 1
A: Type
a00, a01, x: A
px0: a00 = x
px1: a01 = x
p0x: a00 = a01
a: PathSquare px0 px1 p0x 1
px1 = px1 @ 1
    1,2: apply inverse, concat_p1.
  Defined.

End PathSquareConcat.

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

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

  (** There are many more laws to write, but it seems we don't really need them. *)

  Context
    {A : Type}
    {a00 a10 a01 a11 a02 a12 a20 a21 a03 a13 : A} {px0 : a00 = a10}
    {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
    {px2 : a02 = a12} {p0y : a01 = a02} {p1y : a11 = a12}
    {px3 : a03 = a13} {p0z : a02 = a03} {p1z : a12 = a13}
    (s : PathSquare px0 px1 p0x p1x).

  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.A: Type
a00, a10, a01, a11, a02, a12, a20, a21, a03, a13: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px2: a02 = a12
p0y: a01 = a02
p1y: a11 = a12
px3: a03 = a13
p0z: a02 = a03
p1z: a12 = a13
s: PathSquare px0 px1 p0x p1x
s @@h hr = sq_ccGG (concat_p1 p0x)^ (concat_p1 p1x)^ s
  Proof.A: Type
a00, a10, a01, a11, a02, a12, a20, a21, a03, a13: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px2: a02 = a12
p0y: a01 = a02
p1y: a11 = a12
px3: a03 = a13
p0z: a02 = a03
p1z: a12 = a13
s: PathSquare px0 px1 p0x p1x
s @@h hr = sq_ccGG (concat_p1 p0x)^ (concat_p1 p1x)^ s
    by destruct px1.
  Defined.

  Definition sq_concat_h_1s : sq_concat_h hr s = sq_ccGG (concat_1p _)^ (concat_1p _)^ s.A: Type
a00, a10, a01, a11, a02, a12, a20, a21, a03, a13: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px2: a02 = a12
p0y: a01 = a02
p1y: a11 = a12
px3: a03 = a13
p0z: a02 = a03
p1z: a12 = a13
s: PathSquare px0 px1 p0x p1x
hr @@h s = sq_ccGG (concat_1p p0x)^ (concat_1p p1x)^ s
  Proof.A: Type
a00, a10, a01, a11, a02, a12, a20, a21, a03, a13: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px2: a02 = a12
p0y: a01 = a02
p1y: a11 = a12
px3: a03 = a13
p0z: a02 = a03
p1z: a12 = a13
s: PathSquare px0 px1 p0x p1x
hr @@h s = sq_ccGG (concat_1p p0x)^ (concat_1p p1x)^ s
    by destruct s.
  Defined.

  Definition sq_concat_v_s1 : sq_concat_v s vr = sq_GGcc (concat_p1 _)^ (concat_p1 _)^ s.A: Type
a00, a10, a01, a11, a02, a12, a20, a21, a03, a13: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px2: a02 = a12
p0y: a01 = a02
p1y: a11 = a12
px3: a03 = a13
p0z: a02 = a03
p1z: a12 = a13
s: PathSquare px0 px1 p0x p1x
s @@v vr = sq_GGcc (concat_p1 px0)^ (concat_p1 px1)^ s
  Proof.A: Type
a00, a10, a01, a11, a02, a12, a20, a21, a03, a13: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px2: a02 = a12
p0y: a01 = a02
p1y: a11 = a12
px3: a03 = a13
p0z: a02 = a03
p1z: a12 = a13
s: PathSquare px0 px1 p0x p1x
s @@v vr = sq_GGcc (concat_p1 px0)^ (concat_p1 px1)^ s
    by destruct p1x.
  Defined.

  Definition sq_concat_v_1s : sq_concat_v vr s = sq_GGcc (concat_1p _)^ (concat_1p _)^ s.A: Type
a00, a10, a01, a11, a02, a12, a20, a21, a03, a13: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px2: a02 = a12
p0y: a01 = a02
p1y: a11 = a12
px3: a03 = a13
p0z: a02 = a03
p1z: a12 = a13
s: PathSquare px0 px1 p0x p1x
vr @@v s = sq_GGcc (concat_1p px0)^ (concat_1p px1)^ s
  Proof.A: Type
a00, a10, a01, a11, a02, a12, a20, a21, a03, a13: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px2: a02 = a12
p0y: a01 = a02
p1y: a11 = a12
px3: a03 = a13
p0z: a02 = a03
p1z: a12 = a13
s: PathSquare px0 px1 p0x p1x
vr @@v s = sq_GGcc (concat_1p px0)^ (concat_1p px1)^ s
    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
    = sq_ccGG (concat_p_pp _ _ _) (concat_p_pp _ _ _) (sq_concat_h s (sq_concat_h t u)).A: Type
a00, a10, a01, a11, a02, a12, a20, a21, a03, a13: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px2: a02 = a12
p0y: a01 = a02
p1y: a11 = a12
px3: a03 = a13
p0z: a02 = a03
p1z: a12 = a13
s: PathSquare px0 px1 p0x p1x
t: PathSquare px1 px2 p0y p1y
u: PathSquare px2 px3 p0z p1z
(s @@h t) @@h u =
sq_ccGG (concat_p_pp p0x p0y p0z)
  (concat_p_pp p1x p1y p1z) (s @@h (t @@h u))
  Proof.A: Type
a00, a10, a01, a11, a02, a12, a20, a21, a03, a13: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px2: a02 = a12
p0y: a01 = a02
p1y: a11 = a12
px3: a03 = a13
p0z: a02 = a03
p1z: a12 = a13
s: PathSquare px0 px1 p0x p1x
t: PathSquare px1 px2 p0y p1y
u: PathSquare px2 px3 p0z p1z
(s @@h t) @@h u =
sq_ccGG (concat_p_pp p0x p0y p0z)
  (concat_p_pp p1x p1y p1z) (s @@h (t @@h u))
    by destruct s, u, (sq_1G^-1 t), p0y.
  Defined.

End GroupoidLawsH.

(** [PathSquare] Kan fillers ~ Every open box has a lid. *)

Section Kan.

  (** These can be used to prove groupoid laws about paths. *)
  Context {A : Type} {a00 a10 a01 a11 : A}.

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

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

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

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

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}.A: Type
a00, a10, a01, a11: A
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
Contr {px0 : a00 = a10 & PathSquare px0 px1 p0x p1x}
  Proof.A: Type
a00, a10, a01, a11: A
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
Contr {px0 : a00 = a10 & PathSquare px0 px1 p0x p1x}
    apply (Build_Contr _ (sq_fill_l px1 p0x p1x)).A: Type
a00, a10, a01, a11: A
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
forall
y : {px0 : a00 = a10 & PathSquare px0 px1 p0x p1x},
sq_fill_l px1 p0x p1x = y
    intros [px0' s'].A: Type
a00, a10, a01, a11: A
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
px0': a00 = a10
s': PathSquare px0' px1 p0x p1x
sq_fill_l px1 p0x p1x = (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}.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
p0x: a00 = a01
p1x: a10 = a11
Contr {px1 : a01 = a11 & PathSquare px0 px1 p0x p1x}
  Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
p0x: a00 = a01
p1x: a10 = a11
Contr {px1 : a01 = a11 & PathSquare px0 px1 p0x p1x}
    apply (Build_Contr _ (sq_fill_r px0 p0x p1x)).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
p0x: a00 = a01
p1x: a10 = a11
forall
y : {px1 : a01 = a11 & PathSquare px0 px1 p0x p1x},
sq_fill_r px0 p0x p1x = y
    intros [px1' s'].A: Type
a00, a10, a01, a11: A
px0: a00 = a10
p0x: a00 = a01
p1x: a10 = a11
px1': a01 = a11
s': PathSquare px0 px1' p0x p1x
sq_fill_r px0 p0x p1x = (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}.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p1x: a10 = a11
Contr {p0x : a00 = a01 & PathSquare px0 px1 p0x p1x}
  Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p1x: a10 = a11
Contr {p0x : a00 = a01 & PathSquare px0 px1 p0x p1x}
    apply (Build_Contr _ (sq_fill_t px0 px1 p1x)).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p1x: a10 = a11
forall
y : {p0x : a00 = a01 & PathSquare px0 px1 p0x p1x},
sq_fill_t px0 px1 p1x = y
    intros [p0x' s'].A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p1x: a10 = a11
p0x': a00 = a01
s': PathSquare px0 px1 p0x' p1x
sq_fill_t px0 px1 p1x = (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}.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
Contr {p1x : a10 = a11 & PathSquare px0 px1 p0x p1x}
  Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
Contr {p1x : a10 = a11 & PathSquare px0 px1 p0x p1x}
    apply (Build_Contr _ (sq_fill_b px0 px1 p0x)).A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
forall
y : {p1x : a10 = a11 & PathSquare px0 px1 p0x p1x},
sq_fill_b px0 px1 p0x = y
    intros [p1x' s'].A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x': a10 = a11
s': PathSquare px0 px1 p0x p1x'
sq_fill_b px0 px1 p0x = (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.A: Type
a00, a10, a01, a11: A
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
P: forall px0 : a00 = a10,
PathSquare px0 px1 p0x p1x -> Type
fill:= sq_fill_l px1 p0x p1x: {px0 : a00 = a10 & PathSquare px0 px1 p0x p1x}
p: P fill.1 fill.2
forall (px0 : a00 = a10)
(sq : PathSquare px0 px1 p0x p1x), P px0 sq
  Proof.A: Type
a00, a10, a01, a11: A
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
P: forall px0 : a00 = a10,
PathSquare px0 px1 p0x p1x -> Type
fill:= sq_fill_l px1 p0x p1x: {px0 : a00 = a10 & PathSquare px0 px1 p0x p1x}
p: P fill.1 fill.2
forall (px0 : a00 = a10)
(sq : PathSquare px0 px1 p0x p1x), P px0 sq
    intros px0 sq.A: Type
a00, a10, a01, a11: A
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
P: forall px0 : a00 = a10,
PathSquare px0 px1 p0x p1x -> Type
fill:= sq_fill_l px1 p0x p1x: {px0 : a00 = a10 & PathSquare px0 px1 p0x p1x}
p: P fill.1 fill.2
px0: a00 = a10
sq: PathSquare px0 px1 p0x p1x
P 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.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
p0x: a00 = a01
p1x: a10 = a11
P: forall px1 : a01 = a11,
PathSquare px0 px1 p0x p1x -> Type
fill:= sq_fill_r px0 p0x p1x: {px1 : a01 = a11 & PathSquare px0 px1 p0x p1x}
p: P fill.1 fill.2
forall (px1 : a01 = a11)
(sq : PathSquare px0 px1 p0x p1x), P px1 sq
  Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
p0x: a00 = a01
p1x: a10 = a11
P: forall px1 : a01 = a11,
PathSquare px0 px1 p0x p1x -> Type
fill:= sq_fill_r px0 p0x p1x: {px1 : a01 = a11 & PathSquare px0 px1 p0x p1x}
p: P fill.1 fill.2
forall (px1 : a01 = a11)
(sq : PathSquare px0 px1 p0x p1x), P px1 sq
    intros px1 sq.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
p0x: a00 = a01
p1x: a10 = a11
P: forall px1 : a01 = a11,
PathSquare px0 px1 p0x p1x -> Type
fill:= sq_fill_r px0 p0x p1x: {px1 : a01 = a11 & PathSquare px0 px1 p0x p1x}
p: P fill.1 fill.2
px1: a01 = a11
sq: PathSquare px0 px1 p0x p1x
P 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.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p1x: a10 = a11
P: forall p0x : a00 = a01,
PathSquare px0 px1 p0x p1x -> Type
fill:= sq_fill_t px0 px1 p1x: {p0x : a00 = a01 & PathSquare px0 px1 p0x p1x}
p: P fill.1 fill.2
forall (p0x : a00 = a01)
(sq : PathSquare px0 px1 p0x p1x), P p0x sq
  Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p1x: a10 = a11
P: forall p0x : a00 = a01,
PathSquare px0 px1 p0x p1x -> Type
fill:= sq_fill_t px0 px1 p1x: {p0x : a00 = a01 & PathSquare px0 px1 p0x p1x}
p: P fill.1 fill.2
forall (p0x : a00 = a01)
(sq : PathSquare px0 px1 p0x p1x), P p0x sq
    intros p0x sq.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p1x: a10 = a11
P: forall p0x : a00 = a01,
PathSquare px0 px1 p0x p1x -> Type
fill:= sq_fill_t px0 px1 p1x: {p0x : a00 = a01 & PathSquare px0 px1 p0x p1x}
p: P fill.1 fill.2
p0x: a00 = a01
sq: PathSquare px0 px1 p0x p1x
P 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.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
P: forall p1x : a10 = a11,
PathSquare px0 px1 p0x p1x -> Type
fill:= sq_fill_b px0 px1 p0x: {p1x : a10 = a11 & PathSquare px0 px1 p0x p1x}
p: P fill.1 fill.2
forall (p1x : a10 = a11)
(sq : PathSquare px0 px1 p0x p1x), P p1x sq
  Proof.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
P: forall p1x : a10 = a11,
PathSquare px0 px1 p0x p1x -> Type
fill:= sq_fill_b px0 px1 p0x: {p1x : a10 = a11 & PathSquare px0 px1 p0x p1x}
p: P fill.1 fill.2
forall (p1x : a10 = a11)
(sq : PathSquare px0 px1 p0x p1x), P p1x sq
    intros p1x sq.A: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
P: forall p1x : a10 = a11,
PathSquare px0 px1 p0x p1x -> Type
fill:= sq_fill_b px0 px1 p0x: {p1x : a10 = a11 & PathSquare px0 px1 p0x p1x}
p: P fill.1 fill.2
p1x: a10 = a11
sq: PathSquare px0 px1 p0x p1x
P p1x sq
    by destruct sq.
  Defined.

End KanUnique.

(** An interchange law between horizontal and vertical composites in the following square:
<<
            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
>>
*)

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).A: Type
a00, a10, a20, a01, a11, a21, a02, a12, a22: A
vi0: a00 = a10
h0i: a00 = a01
vi1: a01 = a11
h1i: a10 = a11
vj0: a10 = a20
vj1: a11 = a21
h2i: a20 = a21
vi2: a02 = a12
h0j: a01 = a02
h1j: a11 = a12
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.A: Type
a00, a10, a20, a01, a11, a21, a02, a12, a22: A
vi0: a00 = a10
h0i: a00 = a01
vi1: a01 = a11
h1i: a10 = a11
vj0: a10 = a20
vj1: a11 = a21
h2i: a20 = a21
vi2: a02 = a12
h0j: a01 = a02
h1j: a11 = a12
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)
  destruct sq00, sq11.A: Type
a20, a02, x: A
vj0: x = a20
h2i: a20 = x
vi2: a02 = x
h0j: x = a02
sq10: PathSquare vj0 1 1 h2i
sq01: PathSquare 1 vi2 h0j 1
(1%square @@v sq10) @@h (sq01 @@v 1%square) =
(1%square @@h sq01) @@v (sq10 @@h 1%square)
  destruct vi2, h2i.A: Type
a20: A
vj0, h0j: a20 = a20
sq10: PathSquare vj0 1 1 1
sq01: PathSquare 1 1 h0j 1
(1%square @@v sq10) @@h (sq01 @@v 1%square) =
(1%square @@h sq01) @@v (sq10 @@h 1%square)
  revert vj0 sq10; rapply pathsquare_ind_l.A: Type
a20: A
h0j: a20 = a20
sq01: PathSquare 1 1 h0j 1
(1%square @@v (sq_fill_l 1 1 1).2) @@h
(sq01 @@v 1%square) =
(1%square @@h sq01) @@v
((sq_fill_l 1 1 1).2 @@h 1%square)
  reflexivity.
Defined.

(** Squares arising from [ap]. *)

(** 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}
  : PathSquare px0 px1 p0x p1x -> PathSquare (ap f px0) (ap f px1) (ap f p0x) (ap f p1x).A, B: Type
a00, a10, a01, a11: A
f: A -> B
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x ->
PathSquare (ap f px0) (ap f px1) (ap f p0x) (ap f p1x)
Proof.A, B: Type
a00, a10, a01, a11: A
f: A -> B
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
PathSquare px0 px1 p0x p1x ->
PathSquare (ap f px0) (ap f px1) (ap f p0x) (ap f p1x)
  by intros [].
Defined.

(** This preserves reflexivity. *)
Definition sq_ap_refl_h {A B} (f : A -> B) {a0 a1 : A} (p : a0 = a1)
  : sq_ap f (sq_refl_h p) = sq_refl_h (ap f p).A, B: Type
f: A -> B
a0, a1: A
p: a0 = a1
sq_ap f (sq_refl_h p) = sq_refl_h (ap f p)
Proof.A, B: Type
f: A -> B
a0, a1: A
p: a0 = a1
sq_ap f (sq_refl_h p) = sq_refl_h (ap f p)
  by destruct p.
Defined.

Definition sq_ap_refl_v {A B} (f : A -> B) {a0 a1 : A} (p : a0 = a1)
  : sq_ap f (sq_refl_v p) = sq_refl_v (ap f p).A, B: Type
f: A -> B
a0, a1: A
p: a0 = a1
sq_ap f (sq_refl_v p) = sq_refl_v (ap f p)
Proof.A, B: Type
f: A -> B
a0, a1: A
p: a0 = a1
sq_ap f (sq_refl_v p) = sq_refl_v (ap f p)
  by destruct p.
Defined.

(** The naturality square from an [ap]. *)
Definition ap_nat {A B} {f f' : A -> B} (h : f == f') {x y : A} (p : x = y)
  : PathSquare (ap f p) (ap f' p) (h x) (h y).A, B: Type
f, f': A -> B
h: f == f'
x, y: A
p: x = y
PathSquare (ap f p) (ap f' p) (h x) (h y)
Proof.A, B: Type
f, f': A -> B
h: f == f'
x, y: A
p: x = y
PathSquare (ap f p) (ap f' p) (h x) (h y)
  by destruct p; apply sq_1G.
Defined.

(** The transpose of the naturality square. *)
Definition ap_nat' {A B} {f f' : A -> B} (h : f == f') {x y : A} (p : x = y)
  : PathSquare (h x) (h y) (ap f p) (ap f' p).A, B: Type
f, f': A -> B
h: f == f'
x, y: A
p: x = y
PathSquare (h x) (h y) (ap f p) (ap f' p)
Proof.A, B: Type
f, f': A -> B
h: f == f'
x, y: A
p: x = y
PathSquare (h x) (h y) (ap f p) (ap f' p)
  by destruct p; apply sq_G1.
Defined.

(** [ap_compose] fits into a square. *)
Definition ap_compose_sq {A B C} (f : A -> B) (g : B -> C) {x y : A} (p : x = y)
  : PathSquare (ap (g o f) p) (ap g (ap f p)) 1 1 := sq_G1 (ap_compose f g p).

Definition ap_idmap_sq {A} {x y : A} (p : x = y) : PathSquare (ap idmap p) p 1 1
  := sq_G1 (ap_idmap p).

(** A [DPath] of a certain form can be turned into a square. *)
Definition equiv_sq_dp {A B : Type} {f g : A -> B} {a1 a2 : A} {p : a1 = a2}
  {q1 : f a1 = g a1} {q2 : f a2 = g a2}
  : DPath (fun x => f x = g x) p q1 q2 <~> PathSquare q1 q2 (ap f p) (ap g p).A, B: Type
f, g: A -> B
a1, a2: A
p: a1 = a2
q1: f a1 = g a1
q2: f a2 = g a2
DPath (fun x : A => f x = g x) p q1 q2 <~>
PathSquare q1 q2 (ap f p) (ap g p)
Proof.A, B: Type
f, g: A -> B
a1, a2: A
p: a1 = a2
q1: f a1 = g a1
q2: f a2 = g a2
DPath (fun x : A => f x = g x) p q1 q2 <~>
PathSquare q1 q2 (ap f p) (ap g p)
  destruct p.A, B: Type
f, g: A -> B
a1: A
q1, q2: f a1 = g a1
DPath (fun x : A => f x = g x) 1 q1 q2 <~>
PathSquare q1 q2 (ap f 1) (ap g 1)
  exact sq_G1.
Defined.

Notation sq_dp := equiv_sq_dp.

(** [ap011] fits into a square. *)
Definition sq_ap011 {A B C} (f : A -> B -> C)
  {a a' : A} (p : a = a') {b b' : B} (q : b = b')
  : PathSquare (ap (fun x => f x b) p) (ap (fun x => f x b') p)
    (ap (f a) q) (ap (f a') q).A, B, C: Type
f: A -> B -> C
a, a': A
p: a = a'
b, b': B
q: b = b'
PathSquare (ap (fun x : A => f x b) p)
  (ap (fun x : A => f x b') p) (ap (f a) q)
  (ap (f a') q)
Proof.A, B, C: Type
f: A -> B -> C
a, a': A
p: a = a'
b, b': B
q: b = b'
PathSquare (ap (fun x : A => f x b) p)
  (ap (fun x : A => f x b') p) (ap (f a) q)
  (ap (f a') q)
  apply sq_dp.A, B, C: Type
f: A -> B -> C
a, a': A
p: a = a'
b, b': B
q: b = b'
DPath (fun x : B => f a x = f a' x) q
  (ap (fun x : A => f x b) p)
  (ap (fun x : A => f x b') p)
  exact (apD (fun y => ap (fun x => f x y) p) q).
Defined.

(** [PathSquare]s respect products. *)
Definition equiv_sq_prod {A B : Type} {a00 a10 a01 a11 : A} {px0 : a00 = a10}
  {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11} {b00 b10 b01 b11 : B}
  {qx0 : b00 = b10} {qx1 : b01 = b11} {q0x : b00 = b01} {q1x : b10 = b11}
  : (PathSquare px0 px1 p0x p1x) * (PathSquare qx0 qx1 q0x q1x)
    <~> PathSquare (path_prod' px0 qx0) (path_prod' px1 qx1)
        (path_prod' p0x q0x) (path_prod' p1x q1x).A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
PathSquare px0 px1 p0x p1x *
PathSquare qx0 qx1 q0x q1x <~>
PathSquare (path_prod' px0 qx0) (path_prod' px1 qx1)
  (path_prod' p0x q0x) (path_prod' p1x q1x)
Proof.A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
PathSquare px0 px1 p0x p1x *
PathSquare qx0 qx1 q0x q1x <~>
PathSquare (path_prod' px0 qx0) (path_prod' px1 qx1)
  (path_prod' p0x q0x) (path_prod' p1x q1x)
  refine (_ oE (equiv_functor_prod' sq_path sq_path)^-1%equiv).A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
(px0 @ p1x = p0x @ px1) * (qx0 @ q1x = q0x @ qx1) <~>
PathSquare (path_prod' px0 qx0) (path_prod' px1 qx1)
  (path_prod' p0x q0x) (path_prod' p1x q1x)
  refine (_ oE equiv_path_prod (_,_) (_,_)).A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
(px0 @ p1x, qx0 @ q1x) = (p0x @ px1, q0x @ qx1) <~>
PathSquare (path_prod' px0 qx0) (path_prod' px1 qx1)
  (path_prod' p0x q0x) (path_prod' p1x q1x)
  srefine (_ oE equiv_ap' _ _ _).A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
?f (px0 @ p1x, qx0 @ q1x) = ?f (p0x @ px1, q0x @ qx1) <~>
PathSquare (path_prod' px0 qx0) (path_prod' px1 qx1)
  (path_prod' p0x q0x) (path_prod' p1x q1x)
A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
Type
A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
(a00 = a11) * (b00 = b11) <~> ?B
  3: exact (equiv_path_prod (_,_) (_,_)).A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
equiv_path_prod (a00, b00) (a11, b11)
  (px0 @ p1x, qx0 @ q1x) =
equiv_path_prod (a00, b00) (a11, b11)
  (p0x @ px1, q0x @ qx1) <~>
PathSquare (path_prod' px0 qx0) (path_prod' px1 qx1)
  (path_prod' p0x q0x) (path_prod' p1x q1x)
  refine (_ oE equiv_concat_l _^ _).A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
?Goal0 =
equiv_path_prod (a00, b00) (a11, b11)
  (p0x @ px1, q0x @ qx1) <~>
PathSquare (path_prod' px0 qx0) (path_prod' px1 qx1)
  (path_prod' p0x q0x) (path_prod' p1x q1x)
A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
equiv_path_prod (a00, b00) (a11, b11)
  (px0 @ p1x, qx0 @ q1x) = ?Goal0
  2: apply (path_prod_pp (_,_) (_,_) (_,_)).A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
path_prod (a00, b00) (a10, b10) px0 qx0 @
path_prod (a10, b10) (a11, b11) p1x q1x =
equiv_path_prod (a00, b00) (a11, b11)
  (p0x @ px1, q0x @ qx1) <~>
PathSquare (path_prod' px0 qx0) (path_prod' px1 qx1)
  (path_prod' p0x q0x) (path_prod' p1x q1x)
  refine (_ oE equiv_concat_r _ _).A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
path_prod (a00, b00) (a10, b10) px0 qx0 @
path_prod (a10, b10) (a11, b11) p1x q1x = ?Goal0 <~>
PathSquare (path_prod' px0 qx0) (path_prod' px1 qx1)
  (path_prod' p0x q0x) (path_prod' p1x q1x)
A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
equiv_path_prod (a00, b00) (a11, b11)
  (p0x @ px1, q0x @ qx1) = ?Goal0
  2: apply (path_prod_pp (_,_) (_,_) (_,_)).A, B: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00, b10, b01, b11: B
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
path_prod (a00, b00) (a10, b10) px0 qx0 @
path_prod (a10, b10) (a11, b11) p1x q1x =
path_prod (a00, b00) (a01, b01) p0x q0x @
path_prod (a01, b01) (a11, b11) px1 qx1 <~>
PathSquare (path_prod' px0 qx0) (path_prod' px1 qx1)
  (path_prod' p0x q0x) (path_prod' p1x q1x)
  exact sq_path.
Defined.

Notation sq_prod := equiv_sq_prod.