PathSquare.v

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 *)

(* 
        x00 ----pi0---- x01
         |               |
         |               |
        p0i     ==>     p1i
         |               |
         |               |
        x01-----pi1-----x11
 *)

(* Contents:

  * Definition of PathSquare 
  * Degenerate PathSquares as paths between paths
  * Flipping squares horizontally and vertically
  * PathSquare transpose
  * PathSquare inverse
  * PathSquare rotations
  * Edge rewriting
  * Concatenation
  * Kan fillers
  * natural squares from ap

*)

(* Definition of PathSquare *)
(* 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.

Scheme PathSquare_ind := Induction for PathSquare Sort Type.
Arguments PathSquare_ind {A} P f {_ _ _ _ _ _ _ _} _.
Scheme PathSquare_rec := Minimality for PathSquare Sort Type.
Arguments PathSquare_rec {A} P f {_ _ _ _ _ _ _ _} _.

(* PathSquare_ind is an equivalence, similar to how paths_ind is *)
Global 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.

(* PathSquares 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
  snrapply 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 *)
Global 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 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
  apply 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
  apply 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 equvialences. 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
    refine (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
    refine (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
    refine (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
    refine (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
    refine (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
    refine (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.

(* Depdent 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.

  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}
    : 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.

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

End PathSquareConcat.

(* 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).

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

  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
sq_concat_h s 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
sq_concat_h s hr =
sq_ccGG (concat_p1 p0x)^ (concat_p1 p1x)^ s
    by destruct s.
  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
sq_concat_h hr 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
sq_concat_h hr s =
sq_ccGG (concat_1p p0x)^ (concat_1p p1x)^ 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
sq_concat_h (sq_concat_h s t) u =
sq_ccGG (concat_p_pp p0x p0y p0z)
  (concat_p_pp p1x p1y p1z)
  (sq_concat_h s (sq_concat_h t 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
sq_concat_h (sq_concat_h s t) u =
sq_ccGG (concat_p_pp p0x p0y p0z)
  (concat_p_pp p1x p1y p1z)
  (sq_concat_h s (sq_concat_h t 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_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'.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
px0': a00 = a10
s': PathSquare px0' px1 p0x p1x
px0 = px0'
  Proof.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
px0': a00 = a10
s': PathSquare px0' px1 p0x p1x
px0 = px0'
    destruct s.A: Type
x: A
px0': x = x
s': PathSquare px0' 1 1 1
1 = px0'
    apply sq_path^-1 in s'.A: Type
x: A
px0': x = x
s': px0' @ 1 = 1 @ 1
1 = px0'
    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}.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_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'.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
px1': a01 = a11
s': PathSquare px0 px1' p0x p1x
px1 = px1'
  Proof.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
px1': a01 = a11
s': PathSquare px0 px1' p0x p1x
px1 = px1'
    destruct s.A: Type
x: A
px1': x = x
s': PathSquare 1 px1' 1 1
1 = px1'
    apply sq_path^-1 in s'.A: Type
x: A
px1': x = x
s': 1 @ 1 = 1 @ px1'
1 = px1'
    exact (s' @ concat_1p _).
  Defined.

  Definition equiv_sq_fill_lr (p0x : a00 = a01) (p1x : a10 = a11)
    : (a00 = a10) <~> (a01 = a11).A: Type
a00, a10, a01, a11: A
p0x: a00 = a01
p1x: a10 = a11
a00 = a10 <~> a01 = a11
  Proof.A: Type
a00, a10, a01, a11: A
p0x: a00 = a01
p1x: a10 = a11
a00 = a10 <~> a01 = a11
    srapply equiv_adjointify.A: Type
a00, a10, a01, a11: A
p0x: a00 = a01
p1x: a10 = a11
a00 = a10 -> a01 = a11
A: Type
a00, a10, a01, a11: A
p0x: a00 = a01
p1x: a10 = a11
a01 = a11 -> a00 = a10
A: Type
a00, a10, a01, a11: A
p0x: a00 = a01
p1x: a10 = a11
?f o ?g == idmap
A: Type
a00, a10, a01, a11: A
p0x: a00 = a01
p1x: a10 = a11
?g o ?f == idmap
    -A: Type
a00, a10, a01, a11: A
p0x: a00 = a01
p1x: a10 = a11
a00 = a10 -> a01 = a11 intros px0; exact (sq_fill_r px0 p0x p1x).1.
    -A: Type
a00, a10, a01, a11: A
p0x: a00 = a01
p1x: a10 = a11
a01 = a11 -> a00 = a10 intros px1; exact (sq_fill_l px1 p0x p1x).1.
    -A: Type
a00, a10, a01, a11: A
p0x: a00 = a01
p1x: a10 = a11
(fun px0 : a00 = a10 => (sq_fill_r px0 p0x p1x).1)
o (fun px1 : a01 = a11 => (sq_fill_l px1 p0x p1x).1) ==
idmap intros px1.A: Type
a00, a10, a01, a11: A
p0x: a00 = a01
p1x: a10 = a11
px1: a01 = a11
(sq_fill_r (sq_fill_l px1 p0x p1x).1 p0x p1x).1 = px1
      exact (sq_fill_r_uniq (sq_fill_r _ p0x p1x).2
                            (sq_fill_l px1 p0x p1x).2).
    -A: Type
a00, a10, a01, a11: A
p0x: a00 = a01
p1x: a10 = a11
(fun px1 : a01 = a11 => (sq_fill_l px1 p0x p1x).1)
o (fun px0 : a00 = a10 => (sq_fill_r px0 p0x p1x).1) ==
idmap intros px0.A: Type
a00, a10, a01, a11: A
p0x: a00 = a01
p1x: a10 = a11
px0: a00 = a10
(sq_fill_l (sq_fill_r px0 p0x p1x).1 p0x p1x).1 = 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}.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.

(* 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.

(* PathSquares 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: apply (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)
  apply sq_path.
Defined.

Notation sq_prod := equiv_sq_prod.

(* The natural 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 natural 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 naturally 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.