Require Import Basics.
Require Import Cubical.DPath.
Require Import Cubical.PathSquare.
Require Import Cubical.DPathSquare.
Require Import Types.Paths Types.Prod.

Declare Scope cube_scope.
Delimit Scope cube_scope with cube.
Local Unset Elimination Schemes.
Generalizable All Variables.

Local Open Scope square_scope.

(*
x001----pi01----x101              x001----pi01----x101
 |  \               \              |               |  \
 |  p00i  ==si0i=>  p10i           |               |  p10i
p0i1  \               \           p0i1 ==sii1=>   p1i1  \
 |    x000----pi00----x100         |               |    x100
 |s0ii |               |    ===>   |               | s1ii|
x011   |               |          x011----pi11----x111   |
  \   p0i0  ==sii0=>  p1i0          \               \   p1i0
 p01i  |               |           p01i  ==si1i=>  p11i  |
     \ |               |               \               \ |
      x010----pi10----x110              x010----pi10----x110
 *)

Cumulative Inductive PathCube {A}
  : ∀ x000 {x010 x100 x110 x001 x011 x101 x111 : A}
  {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
  {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
  {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
  {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
  (s0ii : PathSquare p0i0 p0i1 p00i p01i) (s1ii : PathSquare p1i0 p1i1 p10i p11i)
  (sii0 : PathSquare p0i0 p1i0 pi00 pi10) (sii1 : PathSquare p0i1 p1i1 pi01 pi11)
  (si0i : PathSquare p00i p10i pi00 pi01) (si1i : PathSquare p01i p11i pi10 pi11), Type
  := idcube : ∀ x, PathCube x 1 1 1 1 1 1.

Arguments PathCube {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}.

Scheme PathCube_ind := Induction for PathCube Sort Type.
Arguments PathCube_ind {A} P f
  {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}.

Scheme PathCube_rec := Minimality for PathCube Sort Type.
Arguments PathCube_rec {A} P f
  {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}.

(* These notations make it easier to write our lemmas *)
Local Notation hr := (sq_refl_h _).
Local Notation vr := (sq_refl_v _).
Local Notation tr := sq_tr.
Local Notation fv := sq_flip_v.

Definition equiv_cu_path {A} {x000 x010 x100 x110 x001 x011 x101 x111 : A}
  {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
  {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
  {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
  {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
  {s0ii : PathSquare p0i0 p0i1 p00i p01i} {s1ii : PathSquare p1i0 p1i1 p10i p11i}
  {sii0 : PathSquare p0i0 p1i0 pi00 pi10} {sii1 : PathSquare p0i1 p1i1 pi01 pi11}
  {si0i : PathSquare p00i p10i pi00 pi01} {si1i : PathSquare p01i p11i pi10 pi11}
  : sq_concat_h (tr (fv s0ii)) (sq_concat_h si0i (tr s1ii)) =
      sq_ccGG
        (moveL_Vp _ _ _ (sq_path^-1 sii0))
        (moveL_Vp _ _ _ (sq_path^-1 sii1)) si1i
      <~> PathCube s0ii s1ii sii0 sii1 si0i si1i.
Proof.
  srapply equiv_adjointify.
  { destruct sii0, sii1; cbn.
    rewrite (eisretr sq_G1 si0i)^,
      (eisretr sq_1G s0ii)^,
      (eisretr sq_1G s1ii)^.
    intro X.
    by destruct (sq_G1^-1 si0i), (sq_1G^-1 s0ii),
      (sq_1G^-1 s1ii), X, p00i. }
  1,2: by intros [].
  destruct sii0, sii1.
  cbn.
  rewrite <- (eisretr sq_G1 si0i).
  rewrite <- (eisretr sq_1G s0ii).
  rewrite <- (eisretr sq_1G s1ii).
  destruct (@equiv_inv _ _ sq_G1 _ si0i).
  destruct (@equiv_inv _ _ sq_1G _ s0ii).
  destruct (@equiv_inv _ _ sq_1G _ s1ii).
  destruct p00i.
  intro X.
  by destruct X.
Defined.

Notation cu_path := equiv_cu_path.

Section Reflexivity.

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

  (* Left right reflexivity *)
  Definition cu_refl_lr (s : PathSquare px0 px1 p0x p1x) : PathCube s s hr hr hr hr.
  Proof.
    by destruct s.
  Defined.

  (* Top bottom reflexivity *)
  Definition cu_refl_tb (s : PathSquare px0 px1 p0x p1x) : PathCube hr hr s s vr vr.
  Proof.
    by destruct s.
  Defined.

  (* Front back reflexivity *)
  Definition cu_refl_fb (s : PathSquare px0 px1 p0x p1x) : PathCube vr vr vr vr s s.
  Proof.
    by destruct s.
  Defined.

End Reflexivity.

(* Lemmas for rewriting faces of cubes *)
Section PathCubeRewriting.

  Context {A} {x000 x010 x100 x110 x001 x011 x101 x111 : A}
    {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
    {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
    {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
    {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
    {s0ii : PathSquare p0i0 p0i1 p00i p01i} {s1ii : PathSquare p1i0 p1i1 p10i p11i}
    {sii0 : PathSquare p0i0 p1i0 pi00 pi10} {sii1 : PathSquare p0i1 p1i1 pi01 pi11}
    {si0i : PathSquare p00i p10i pi00 pi01} {si1i : PathSquare p01i p11i pi10 pi11}.

  (* We write the most general version and derive special cases from this *)
  Definition equiv_cu_GGGGGG {s0ii' s1ii' sii0' sii1' si0i' si1i'}
    (t0ii : s0ii = s0ii') (t1ii : s1ii = s1ii') (tii0 : sii0 = sii0')
    (tii1 : sii1 = sii1') (ti0i : si0i = si0i') (ti1i : si1i = si1i')
    : PathCube s0ii s1ii sii0 sii1 si0i si1i
    <~> PathCube s0ii' s1ii' sii0' sii1' si0i' si1i'.
  Proof.
    by destruct t0ii, t1ii, tii0, tii1, ti0i, ti1i.
  Defined.

  Context {s0ii' s1ii' sii0' sii1' si0i' si1i'}
    (t0ii : s0ii = s0ii') (t1ii : s1ii = s1ii') (tii0 : sii0 = sii0')
    (tii1 : sii1 = sii1') (ti0i : si0i = si0i') (ti1i : si1i = si1i').

  Definition equiv_cu_Gccccc := equiv_cu_GGGGGG t0ii 1 1 1 1 1.
  Definition equiv_cu_cGcccc := equiv_cu_GGGGGG 1 t1ii 1 1 1 1.
  Definition equiv_cu_ccGccc := equiv_cu_GGGGGG 1 1 tii0 1 1 1.
  Definition equiv_cu_cccGcc := equiv_cu_GGGGGG 1 1 1 tii1 1 1.
  Definition equiv_cu_ccccGc := equiv_cu_GGGGGG 1 1 1 1 ti0i 1.
  Definition equiv_cu_cccccG := equiv_cu_GGGGGG 1 1 1 1 1 ti1i.
  Definition equiv_cu_ccGGGG := equiv_cu_GGGGGG 1 1 tii0 tii1 ti0i ti1i.
  Definition equiv_cu_GGGGcc := equiv_cu_GGGGGG t0ii t1ii tii0 tii1 1 1.
  Definition equiv_cu_GGcccc := equiv_cu_GGGGGG t0ii t1ii 1 1 1 1.
  Definition equiv_cu_ccGGcc := equiv_cu_GGGGGG 1 1 tii0 tii1 1 1.
  Definition equiv_cu_ccccGG := equiv_cu_GGGGGG 1 1 1 1 ti0i ti1i.

End PathCubeRewriting.

Notation cu_GGGGGG := equiv_cu_GGGGGG.
Notation cu_Gccccc := equiv_cu_Gccccc.
Notation cu_cGcccc := equiv_cu_cGcccc.
Notation cu_ccGccc := equiv_cu_ccGccc.
Notation cu_cccGcc := equiv_cu_cccGcc.
Notation cu_ccccGc := equiv_cu_ccccGc.
Notation cu_cccccG := equiv_cu_cccccG.
Notation cu_ccGGGG := equiv_cu_ccGGGG.
Notation cu_GGGGcc := equiv_cu_GGGGcc.
Notation cu_GGcccc := equiv_cu_GGcccc.
Notation cu_ccGGcc := equiv_cu_ccGGcc.
Notation cu_ccccGG := equiv_cu_ccccGG.

(* Rotating top and bottom to front and back *)
Definition equiv_cu_rot_tb_fb {A} {x000 x010 x100 x110 x001 x011 x101 x111 : A}
  {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
  {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
  {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
  {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
  {s0ii : PathSquare p0i0 p0i1 p00i p01i} {s1ii : PathSquare p1i0 p1i1 p10i p11i}
  {sii0 : PathSquare p0i0 p1i0 pi00 pi10} {sii1 : PathSquare p0i1 p1i1 pi01 pi11}
  {si0i : PathSquare p00i p10i pi00 pi01} {si1i : PathSquare p01i p11i pi10 pi11}
  : PathCube si0i si1i (sq_tr s0ii) (sq_tr s1ii) (sq_tr sii0) (sq_tr sii1)
    <~> PathCube s0ii s1ii sii0 sii1 si0i si1i.
Proof.
  srapply equiv_adjointify.
  { intro cube.
    refine (cu_GGGGcc _ _ _ _ _).
    1,2,3,4: exact (eissect tr _).
    revert cube.
    set (a := tr s0ii).
    set (b := tr s1ii).
    set (c := tr sii0).
    set (d := tr sii1).
    clearbody a b c d; clear s0ii s1ii sii0 sii1.
    intro cube.
    by destruct cube. }
  1,2 : by intros [].
  rewrite <- (eissect tr s0ii).
  rewrite <- (eissect tr s1ii).
  rewrite <- (eissect tr sii0).
  rewrite <- (eissect tr sii1).
  set (a := tr s0ii).
  set (b := tr s1ii).
  set (c := tr sii0).
  set (d := tr sii1).
  clearbody a b c d; clear s0ii s1ii sii0 sii1.
  intro X.
  rewrite <- (eissect (cu_ccGGGG (eisretr tr _)
    (eisretr tr _) (eisretr tr _) (eisretr tr _)) X).
  set (e := cu_ccGGGG (eisretr tr _) (eisretr tr _)
    (eisretr tr _) (eisretr tr _) X).
  clearbody e; clear X.
  by destruct e.
Defined.

Notation cu_rot_tb_fb := equiv_cu_rot_tb_fb.

Definition equiv_cu_G11 {A} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11}
  {p0x : a00 = a01} {p1x : a10 = a11}
  {s s' : PathSquare px0 px1 p0x p1x}
  : s = s' <~> PathCube s s' hr hr hr hr.
Proof.
  destruct s.
  refine (cu_path oE _).
  refine (equiv_concat_l (sq_concat_h_1s (sq_concat_h 1%square (tr s'))
    (p0y:=1) (p1y:=1)) _ oE _).
  refine (equiv_concat_l (sq_concat_h_1s (tr s')
    (p0y:=1) (p1y:=1)) _ oE _).
  refine (equiv_moveR_equiv_M (f:=tr) _ _ oE _).
  apply equiv_path_inverse.
Defined.

Definition equiv_cu_1G1 {A} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11}
  {p0x : a00 = a01} {p1x : a10 = a11}
  {s s' : PathSquare px0 px1 p0x p1x}
: s = s' <~> PathCube hr hr s s' vr vr.
Proof.
  refine (cu_rot_tb_fb oE _).
  refine (cu_rot_tb_fb oE _).
  refine (cu_ccGGGG _ _ _ _ oE _).
  1,2: exact sq_tr_refl_v^.
  1,2: exact (eisretr tr _)^.
  refine (_ oE equiv_ap' tr _ _).
  exact equiv_cu_G11.
Defined.

Definition equiv_cu_11G {A} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11}
  {p0x : a00 = a01} {p1x : a10 = a11}
  {s s' : PathSquare px0 px1 p0x p1x}
  : s = s' <~> PathCube vr vr vr vr s s'.
Proof.
  refine (cu_rot_tb_fb oE _).
  refine (cu_ccGGGG _ _ _ _ oE _).
  1-4: exact sq_tr_refl_v^.
  by exact equiv_cu_G11.
Defined.

Notation cu_G11 := equiv_cu_G11.
Notation cu_1G1 := equiv_cu_1G1.
Notation cu_11G := equiv_cu_11G.

Section PathPathSquares.

  Context {A} {x y : A} {a00 a10 a01 a11 : x = y}
    (px0 : a00 = a10) (px1 : a01 = a11)
    (p0x : a00 = a01) (p1x : a10 = a11).

  Definition equiv_cu_GG1
    : PathSquare px0 px1 p0x p1x
      <~> PathCube (sq_G1 px0) (sq_G1 px1) (sq_G1 p0x) (sq_G1 p1x) 1 1.
  Proof.
    destruct p0x, p1x, a00.
    refine (_ oE sq_G1^-1).
    refine (_ oE equiv_ap' sq_G1 _ _).
    exact cu_G11.
  Defined.

  Definition equiv_cu_1GG
    : PathSquare px0 px1 p0x p1x
    <~> PathCube 1 1 (sq_1G px0) (sq_1G px1) (sq_1G p0x) (sq_1G p1x).
  Proof.
    destruct px0, px1, a01.
    refine(_ oE sq_1G^-1).
    refine (_ oE equiv_ap' sq_1G _ _).
    exact cu_11G.
  Defined.

  Definition equiv_cu_G1G : PathSquare px0 px1 p0x p1x
    <~> PathCube (sq_1G px0) (sq_1G px1) 1 1 (sq_G1 p0x) (sq_G1 p1x).
  Proof.
    destruct p0x, p1x, a10.
    refine(_ oE sq_G1^-1).
    refine (_ oE equiv_ap' sq_1G _ _).
    exact cu_G11.
  Defined.

End PathPathSquares.

Notation cu_GG1 := equiv_cu_GG1.
Notation cu_G1G := equiv_cu_G1G.
Notation cu_1GG := equiv_cu_1GG.
Arguments cu_GG1 {_ _ _ _ _ _ _ _ _ _ _}.
Arguments cu_G1G {_ _ _ _ _ _ _ _ _ _ _}.
Arguments cu_1GG {_ _ _ _ _ _ _ _ _ _ _}.

Definition equiv_cu_ds
  {A B} {f g : A → B} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11}
  {p0x : a00 = a01} {p1x : a10 = a11}
  {s : PathSquare px0 px1 p0x p1x}
  {b00 : f a00 = g a00} {b01 : f a01 = g a01}
  {b10 : f a10 = g a10} {b11 : f a11 = g a11}
  {qx0 : DPath (fun x ⇒ f x = g x) px0 b00 b10}
  {qx1 : DPath (fun x ⇒ f x = g x) px1 b01 b11}
  {q0x : DPath (fun x ⇒ f x = g x) p0x b00 b01}
  {q1x : DPath (fun x ⇒ f x = g x) p1x b10 b11}
  : DPathSquare (fun x ⇒ f x = g x) s qx0 qx1 q0x q1x
    <~> PathCube (sq_dp qx0) (sq_dp qx1) (sq_dp q0x) (sq_dp q1x)
      (sq_ap f s) (sq_ap g s).
Proof.
  destruct s.
  exact cu_GG1.
Defined.

Notation cu_ds := equiv_cu_ds.

Definition equiv_dp_cu {A B : Type} {x1 x2 : A} {a00 a01 a10 a11 : A → B}
  {px0 : a00 == a10} {px1 : a01 == a11} {p0x : a00 == a01} {p1x : a10 == a11}
  {f1 : PathSquare (px0 x1) (px1 x1) (p0x x1) (p1x x1)}
  {f2 : PathSquare (px0 x2) (px1 x2) (p0x x2) (p1x x2)}
  {p : x1 = x2}
  : PathCube f1 f2 (sq_dp (apD px0 p)) (sq_dp (apD px1 p))
     (sq_dp (apD p0x p)) (sq_dp (apD p1x p))
  <~> DPath (fun x ⇒ PathSquare (px0 x) (px1 x) (p0x x) (p1x x)) p f1 f2.
Proof.
  destruct p; symmetry; exact cu_G11.
Defined.

Notation dp_cu := equiv_dp_cu.

Definition equiv_cu_flip_lr {A} {x000 x010 x100 x110 x001 x011 x101 x111 : A}
  {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
  {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
  {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
  {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
  {s0ii : PathSquare p0i0 p0i1 p00i p01i} {s1ii : PathSquare p1i0 p1i1 p10i p11i}
  {sii0 : PathSquare p0i0 p1i0 pi00 pi10} {sii1 : PathSquare p0i1 p1i1 pi01 pi11}
  {si0i : PathSquare p00i p10i pi00 pi01} {si1i : PathSquare p01i p11i pi10 pi11}
  : PathCube s0ii s1ii sii0 sii1 si0i si1i
    <~> PathCube s1ii s0ii (sq_flip_h sii0) (sq_flip_h sii1)
        (sq_flip_h si0i) (sq_flip_h si1i).
Proof.
  destruct si1i, si0i.
  refine (cu_GGcccc _ _ oE _).
  1,2: exact (eisretr sq_G1 _).
  refine (cu_GG1 oE _).
  refine (sq_flip_h oE _).
  refine (cu_GG1^-1 oE _).
  refine (cu_GGGGcc _ _ _ _).
  all: exact (eisretr sq_G1 _)^.
Defined.

Notation cu_flip_lr := equiv_cu_flip_lr.

Definition cu_fill_left {A} {x000 x010 x100 x110 x001 x011 x101 x111 : A}
  {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
  {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
  {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
  {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
                                          (s1ii : PathSquare p1i0 p1i1 p10i p11i)
  (sii0 : PathSquare p0i0 p1i0 pi00 pi10) (sii1 : PathSquare p0i1 p1i1 pi01 pi11)
  (si0i : PathSquare p00i p10i pi00 pi01) (si1i : PathSquare p01i p11i pi10 pi11)
  : {s0ii : PathSquare p0i0 p0i1 p00i p01i & PathCube s0ii s1ii sii0 sii1 si0i si1i}.
Proof.
  destruct si0i, si1i.
  set (a := sq_G1^-1 s1ii).
  set (b := sq_G1^-1 sii0).
  set (c := sq_G1^-1 sii1).
  rewrite <- (eisretr sq_G1 s1ii).
  rewrite <- (eisretr sq_G1 sii0).
  rewrite <- (eisretr sq_G1 sii1).
  change (sq_G1^-1 s1ii) with a.
  change (sq_G1^-1 sii0) with b.
  change (sq_G1^-1 sii1) with c.
  clearbody a b c.
  clear s1ii sii0 sii1.
  refine (sq_G1 (b @ a @ c^); _).
  by destruct a, b, c, p0i1.
Defined.

Definition cu_fill_right {A} {x000 x010 x100 x110 x001 x011 x101 x111 : A}
  {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
  {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
  {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
  {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
  (s0ii : PathSquare p0i0 p0i1 p00i p01i)
  (sii0 : PathSquare p0i0 p1i0 pi00 pi10) (sii1 : PathSquare p0i1 p1i1 pi01 pi11)
  (si0i : PathSquare p00i p10i pi00 pi01) (si1i : PathSquare p01i p11i pi10 pi11)
  : {s1ii : PathSquare p1i0 p1i1 p10i p11i & PathCube s0ii s1ii sii0 sii1 si0i si1i}.
Proof.
  refine (_;_).
  apply cu_flip_lr^-1.
  apply cu_fill_left.
Defined.

Definition cu_fill_top {A} {x000 x010 x100 x110 x001 x011 x101 x111 : A}
  {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
  {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
  {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
  {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
  (s0ii : PathSquare p0i0 p0i1 p00i p01i) (s1ii : PathSquare p1i0 p1i1 p10i p11i)
                                          (sii1 : PathSquare p0i1 p1i1 pi01 pi11)
  (si0i : PathSquare p00i p10i pi00 pi01) (si1i : PathSquare p01i p11i pi10 pi11)
  : {sii0 : PathSquare p0i0 p1i0 pi00 pi10 & PathCube s0ii s1ii sii0 sii1 si0i si1i}.
Proof.
  refine (_;_).
  apply cu_rot_tb_fb.
  apply cu_rot_tb_fb.
  refine (cu_Gccccc (eisretr tr _)^ _).
  apply cu_fill_left.
Defined.

Definition cu_fill_bottom {A} {x000 x010 x100 x110 x001 x011 x101 x111 : A}
  {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
  {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
  {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
  {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
  (s0ii : PathSquare p0i0 p0i1 p00i p01i) (s1ii : PathSquare p1i0 p1i1 p10i p11i)
  (sii0 : PathSquare p0i0 p1i0 pi00 pi10)
  (si0i : PathSquare p00i p10i pi00 pi01) (si1i : PathSquare p01i p11i pi10 pi11)
  : {sii1 : PathSquare p0i1 p1i1 pi01 pi11 & PathCube s0ii s1ii sii0 sii1 si0i si1i}.
Proof.
  refine (_;_).
  apply cu_rot_tb_fb.
  apply cu_rot_tb_fb.
  refine (cu_cGcccc (eisretr tr _)^ _).
  apply cu_fill_right.
Defined.

Definition cu_fill_front {A} {x000 x010 x100 x110 x001 x011 x101 x111 : A}
  {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
  {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
  {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
  {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
  (s0ii : PathSquare p0i0 p0i1 p00i p01i) (s1ii : PathSquare p1i0 p1i1 p10i p11i)
  (sii0 : PathSquare p0i0 p1i0 pi00 pi10) (sii1 : PathSquare p0i1 p1i1 pi01 pi11)
                                          (si1i : PathSquare p01i p11i pi10 pi11)
  : {si0i : PathSquare p00i p10i pi00 pi01 & PathCube s0ii s1ii sii0 sii1 si0i si1i}.
Proof.
  refine (_;_).
  apply cu_rot_tb_fb.
  apply cu_fill_left.
Defined.

Definition cu_fill_back {A} {x000 x010 x100 x110 x001 x011 x101 x111 : A}
  {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
  {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
  {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
  {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
  (s0ii : PathSquare p0i0 p0i1 p00i p01i) (s1ii : PathSquare p1i0 p1i1 p10i p11i)
  (sii0 : PathSquare p0i0 p1i0 pi00 pi10) (sii1 : PathSquare p0i1 p1i1 pi01 pi11)
  (si0i : PathSquare p00i p10i pi00 pi01)
  : {si1i : PathSquare p01i p11i pi10 pi11 & PathCube s0ii s1ii sii0 sii1 si0i si1i}.
Proof.
  refine (_;_).
  apply cu_rot_tb_fb.
  apply cu_fill_right.
Defined.

Section Concat.

  Context {A : Type}
    (* Main Cube *)
    {x000 x010 x100 x110 x001 x011 x101 x111 : A}
    {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
    {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
    {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
    {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
    {s0ii : PathSquare p0i0 p0i1 p00i p01i} {s1ii : PathSquare p1i0 p1i1 p10i p11i}
    {sii0 : PathSquare p0i0 p1i0 pi00 pi10} {sii1 : PathSquare p0i1 p1i1 pi01 pi11}
    {si0i : PathSquare p00i p10i pi00 pi01} {si1i : PathSquare p01i p11i pi10 pi11}
    (ciii : PathCube s0ii s1ii sii0 sii1 si0i si1i).

  Definition cu_concat_lr
    {x201 x200 x210 x211 : A}
    {pj01 : x101 = x201} {pj11 : x111 = x211} {pj10 : x110 = x210}
    {pj00 : x100 = x200} {p2i1 : x201 = x211} {p2i0 : x200 = x210}
    {p20i : x200 = x201} {p21i : x210 = x211}
    {sji0 : PathSquare p1i0 p2i0 pj00 pj10} {sji1 : PathSquare p1i1 p2i1 pj01 pj11}
    {sj0i : PathSquare p10i p20i pj00 pj01} {sj1i : PathSquare p11i p21i pj10 pj11}
    {s2ii : PathSquare p2i0 p2i1 p20i p21i}
    (cjii : PathCube s1ii s2ii sji0 sji1 sj0i sj1i)
    : PathCube s0ii s2ii (sq_concat_h sii0 sji0) (sq_concat_h sii1 sji1)
        (sq_concat_h si0i sj0i) (sq_concat_h si1i sj1i).
  Proof.
    destruct cjii, pi00, pi01, pi10, pi11.
    exact ciii.
  Defined.

  Definition cu_concat_tb
    {x020 x021 x120 x121 : A}
    {p0j0 : x010 = x020} {p1j0 : x110 = x120} {p0j1 : x011 = x021}
    {p1j1 : x111 = x121} {p02i : x020 = x021} {p12i : x120 = x121}
    {pi20 : x020 = x120} {pi21 : x021 = x121}
    {s0ji : PathSquare p0j0 p0j1 p01i p02i} {s1ji : PathSquare p1j0 p1j1 p11i p12i}
    {sij0 : PathSquare p0j0 p1j0 pi10 pi20} {sij1 : PathSquare p0j1 p1j1 pi11 pi21}
    {si2i : PathSquare p02i p12i pi20 pi21}
    (ciji : PathCube s0ji s1ji sij0 sij1 si1i si2i)
    : PathCube (sq_concat_v s0ii s0ji) (sq_concat_v s1ii s1ji)
        (sq_concat_v sii0 sij0) (sq_concat_v sii1 sij1) si0i si2i.
  Proof.
    destruct ciji, p0i0, p1i0, p0i1, p1i1.
    exact ciii.
  Defined.

  Definition cu_concat_fb
    {x002 x012 x102 x112 : A}
    {p0i2 : x002 = x012} {p00j : x001 = x002} {p01j : x011 = x012}
    {p1i2 : x102 = x112} {p10j : x101 = x102} {p11j : x111 = x112}
    {pi02 : x002 = x102} {pi12 : x012 = x112}
    {s0ij : PathSquare p0i1 p0i2 p00j p01j} {s1ij : PathSquare p1i1 p1i2 p10j p11j}
    {si0j : PathSquare p00j p10j pi01 pi02} {si1j : PathSquare p01j p11j pi11 pi12}
    {sii2 : PathSquare p0i2 p1i2 pi02 pi12}
    (ciij : PathCube s0ij s1ij sii1 sii2 si0j si1j)
    : PathCube (sq_concat_h s0ii s0ij) (sq_concat_h s1ii s1ij)
        sii0 sii2 (sq_concat_v si0i si0j) (sq_concat_v si1i si1j).
  Proof.
    destruct ciij, p00i, p10i, p11i, p01i.
    exact ciii.
  Defined.

End Concat.

(* Notation for left right concatenation *)
Notation "x '@lr' y" := (cu_concat_lr x y) : cube_scope.

Local Notation apc := (ap_compose_sq _ _ _).

Definition sq_ap_compose {A B C : Type} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
  (f : A → B) (g : B → C) (s : PathSquare px0 px1 p0x p1x)
  : PathCube (sq_ap (g o f) s) (sq_ap g (sq_ap f s)) apc apc apc apc.
Proof.
  by destruct s.
Defined.

Local Notation api := (ap_idmap_sq _).

Definition sq_ap_idmap {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)
  : PathCube (sq_ap idmap s) s api api api api.
Proof.
  by destruct s.
Defined.

Local Notation apn := (ap_nat _ _).

Definition sq_ap_nat
  {A B : Type} {a00 a10 a01 a11 : A} (f f' : A → B) (h : f == f')
  {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
  (s : PathSquare px0 px1 p0x p1x)
  : PathCube (sq_ap f s) (sq_ap f' s) (ap_nat h _) apn apn apn.
Proof.
  destruct s as [x]; cbn; by destruct (h x).
Defined.

Definition sq_ap_uncurry {A B C} (f : A → B → C)
  {a a' : A} (p : a = a') {b b' : B} (q : b = b')
  : PathCube (sq_ap (uncurry f) (sq_prod (hr, vr))) (sq_ap011 f p q)
    (sq_G1 (ap_uncurry _ _ _)) (sq_G1 (ap_uncurry _ _ _))
    (sq_G1 (ap_uncurry _ _ _)) (sq_G1 (ap_uncurry _ _ _)).
Proof.
  by destruct p, q.
Defined.

Definition cu_ap {A B} {x000 x010 x100 x110 x001 x011 x101 x111 : A}
  {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
  {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
  {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001}
  {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111}
  {s0ii : PathSquare p0i0 p0i1 p00i p01i} {s1ii : PathSquare p1i0 p1i1 p10i p11i}
  {sii0 : PathSquare p0i0 p1i0 pi00 pi10} {sii1 : PathSquare p0i1 p1i1 pi01 pi11}
  {si0i : PathSquare p00i p10i pi00 pi01} {si1i : PathSquare p01i p11i pi10 pi11}
  (f : A → B) (c : PathCube s0ii s1ii sii0 sii1 si0i si1i)
  : PathCube (sq_ap f s0ii) (sq_ap f s1ii) (sq_ap f sii0)
     (sq_ap f sii1) (sq_ap f si0i) (sq_ap f si1i).
Proof.
  by destruct c.
Defined.