DPathSquare.v

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

Declare Scope dsquare_scope.
Delimit Scope dsquare_scope with dsquare.

Local Open Scope dpath_scope.

(** Dependent squares *)

Definition DPathSquare {A} (P : A -> Type) {a00 a10 a01 a11}
  {px0 : a00 = a10} {px1 : a01 = a11} {p0x p1x}
  (s : PathSquare px0 px1 p0x p1x) {b00 b10 b01 b11}
  (qx0 : DPath P px0 b00 b10) (qx1 : DPath P px1 b01 b11)
  (q0x : DPath P p0x b00 b01) (q1x : DPath P p1x b10 b11) : Type.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
Type
Proof.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
Type
  destruct s.A: Type
P: A -> Type
x: A
b00, b10, b01, b11: P x
qx0: DPath P 1 b00 b10
qx1: DPath P 1 b01 b11
q0x: DPath P 1 b00 b01
q1x: DPath P 1 b10 b11
Type
  exact (PathSquare qx0 qx1 q0x q1x).
Defined.

Definition ds_id {A} {P : A -> Type} {a00 b00}
  : DPathSquare P sq_id 1 1 1 1 (a00:=a00) (b00:=b00).A: Type
P: A -> Type
a00: A
b00: P a00
DPathSquare P 1%square 1 1 1 1
Proof.A: Type
P: A -> Type
a00: A
b00: P a00
DPathSquare P 1%square 1 1 1 1
  exact sq_id.
Defined.

Notation "1" := ds_id : dsquare_scope.

Section DPathSquareConstructors.

  (** Different ways of constructing dependent squares *)

  Context {A} {a0 a1 : A} {p : a0 = a1} {P : A -> Type}
    {b0 b1} (dp : DPath P p b0 b1).

  Definition ds_refl_h : DPathSquare P (sq_refl_h _) dp dp 1 1.A: Type
a0, a1: A
p: a0 = a1
P: A -> Type
b0: P a0
b1: P a1
dp: DPath P p b0 b1
DPathSquare P (sq_refl_h p) dp dp 1 1
  Proof.A: Type
a0, a1: A
p: a0 = a1
P: A -> Type
b0: P a0
b1: P a1
dp: DPath P p b0 b1
DPathSquare P (sq_refl_h p) dp dp 1 1
    destruct p.A: Type
a0: A
p: a0 = a0
P: A -> Type
b0, b1: P a0
dp: DPath P 1 b0 b1
DPathSquare P (sq_refl_h 1) dp dp 1 1
    apply sq_refl_h.
  Defined.

  Definition ds_refl_v : DPathSquare P (sq_refl_v _) 1 1 dp dp.A: Type
a0, a1: A
p: a0 = a1
P: A -> Type
b0: P a0
b1: P a1
dp: DPath P p b0 b1
DPathSquare P (sq_refl_v p) 1 1 dp dp
  Proof.A: Type
a0, a1: A
p: a0 = a1
P: A -> Type
b0: P a0
b1: P a1
dp: DPath P p b0 b1
DPathSquare P (sq_refl_v p) 1 1 dp dp
    destruct p.A: Type
a0: A
p: a0 = a0
P: A -> Type
b0, b1: P a0
dp: DPath P 1 b0 b1
DPathSquare P (sq_refl_v 1) 1 1 dp dp
    apply sq_refl_v.
  Defined.

End DPathSquareConstructors.

(** [DPathSquare]s can be given by 2-dimensional [DPath]s *)
Definition equiv_ds_dpath {A} (P : A -> Type) {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11}
  {p0x : a00 = a01} {p1x : a10 = a11}
  (s : px0 @ p1x = p0x @ px1) {b00 b10 b01 b11}
  {qx0 : DPath P px0 b00 b10} {qx1 : DPath P px1 b01 b11}
  {q0x : DPath P p0x b00 b01} {q1x : DPath P p1x b10 b11}
  : DPath (fun p => DPath P p b00 b11) s (qx0 @Dp q1x) (q0x @Dp qx1)
    <~> DPathSquare P (sq_path s) qx0 qx1 q0x q1x.A: Type
P: A -> Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
s: px0 @ p1x = p0x @ px1
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
DPath (fun p : a00 = a11 => DPath P p b00 b11) s
  (qx0 @Dp q1x) (q0x @Dp qx1) <~>
DPathSquare P (sq_path s) qx0 qx1 q0x q1x
Proof.A: Type
P: A -> Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
s: px0 @ p1x = p0x @ px1
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
DPath (fun p : a00 = a11 => DPath P p b00 b11) s
  (qx0 @Dp q1x) (q0x @Dp qx1) <~>
DPathSquare P (sq_path s) qx0 qx1 q0x q1x
  set (s' := sq_path s).A: Type
P: A -> Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
s: px0 @ p1x = p0x @ px1
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
s':= sq_path s: PathSquare px0 px1 p0x p1x
DPath (fun p : a00 = a11 => DPath P p b00 b11) s
  (qx0 @Dp q1x) (q0x @Dp qx1) <~>
DPathSquare P s' qx0 qx1 q0x q1x
  rewrite <- (eissect sq_path s : sq_path^-1 s' = s).A: Type
P: A -> Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
s: px0 @ p1x = p0x @ px1
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
s':= sq_path s: PathSquare px0 px1 p0x p1x
DPath (fun p : a00 = a11 => DPath P p b00 b11)
  (sq_path^-1 s') (qx0 @Dp q1x) (q0x @Dp qx1) <~>
DPathSquare P s' qx0 qx1 q0x q1x
  clearbody s'; clear s.A: Type
P: A -> Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
s': PathSquare px0 px1 p0x p1x
DPath (fun p : a00 = a11 => DPath P p b00 b11)
  (sq_path^-1 s') (qx0 @Dp q1x) (q0x @Dp qx1) <~>
DPathSquare P s' qx0 qx1 q0x q1x
  destruct s'; cbn.A: Type
P: A -> Type
x: A
b00, b10, b01, b11: P x
qx0: DPath P 1 b00 b10
qx1: DPath P 1 b01 b11
q0x: DPath P 1 b00 b01
q1x: DPath P 1 b10 b11
qx0 @ q1x = q0x @ qx1 <~> PathSquare qx0 qx1 q0x q1x
  exact sq_path.
Defined.

Notation ds_dpath := equiv_ds_dpath.

(** We have an [apD] for [DPathSquare]s *)
Definition ds_apD {A} {B : A -> Type} (f : forall a, B a) {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11} {p0x p1x} (s : PathSquare px0 px1 p0x p1x)
  : DPathSquare B s (apD f px0) (apD f px1) (apD f p0x) (apD f p1x).A: Type
B: A -> Type
f: forall a : A, B a
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
s: PathSquare px0 px1 p0x p1x
DPathSquare B s (apD f px0) (apD f px1) (apD f p0x)
  (apD f p1x)
Proof.A: Type
B: A -> Type
f: forall a : A, B a
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
s: PathSquare px0 px1 p0x p1x
DPathSquare B s (apD f px0) (apD f px1) (apD f p0x)
  (apD f p1x)
  by destruct s.
Defined.

(* A [DPathSquare] over a constant family is given by just a square *)
Definition ds_const {A P : Type} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
  {s : PathSquare px0 px1 p0x p1x} {b00 b10 b01 b11 : P}
  {qx0 : b00 = b10} {qx1 : b01 = b11} {q0x : b00 = b01} {q1x : b10 = b11}
  : PathSquare qx0 qx1 q0x q1x <~> DPathSquare (fun _ => P) s (dp_const qx0)
      (dp_const qx1) (dp_const q0x) (dp_const q1x).A, P: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
s: PathSquare px0 px1 p0x p1x
b00, b10, b01, b11: P
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
PathSquare qx0 qx1 q0x q1x <~>
DPathSquare (fun _ : A => P) s (dp_const qx0)
  (dp_const qx1) (dp_const q0x) (dp_const q1x)
Proof.A, P: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
s: PathSquare px0 px1 p0x p1x
b00, b10, b01, b11: P
qx0: b00 = b10
qx1: b01 = b11
q0x: b00 = b01
q1x: b10 = b11
PathSquare qx0 qx1 q0x q1x <~>
DPathSquare (fun _ : A => P) s (dp_const qx0)
  (dp_const qx1) (dp_const q0x) (dp_const q1x)
  by destruct s.
Defined.

(* Sometimes we want the DPathSquare to be typed differently *)
(* This could be achieved with some clever rewriting of squares and DPathSquares *)
(* It seems that writing it like this might get in the way, Cube.v has
   some examples of this. *)
Definition equiv_ds_const' {A P : Type} {a00 a10 a01 a11 : A}
  {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
  {s : PathSquare px0 px1 p0x p1x} {b00 b10 b01 b11 : P}
  {qx0 : DPath (fun _ => P) px0 b00 b10}
  {qx1 : DPath (fun _ => P) px1 b01 b11}
  {q0x : DPath (fun _ => P) p0x b00 b01}
  {q1x : DPath (fun _ => P) p1x b10 b11}
  : PathSquare (dp_const^-1 qx0) (dp_const^-1 qx1)
    (dp_const^-1 q0x) (dp_const^-1 q1x)
    <~> DPathSquare (fun _ => P) s qx0 qx1 q0x q1x.A, P: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
s: PathSquare px0 px1 p0x p1x
b00, b10, b01, b11: P
qx0: DPath (fun _ : A => P) px0 b00 b10
qx1: DPath (fun _ : A => P) px1 b01 b11
q0x: DPath (fun _ : A => P) p0x b00 b01
q1x: DPath (fun _ : A => P) p1x b10 b11
PathSquare (dp_const^-1 qx0) (dp_const^-1 qx1)
  (dp_const^-1 q0x) (dp_const^-1 q1x) <~>
DPathSquare (fun _ : A => P) s qx0 qx1 q0x q1x
Proof.A, P: Type
a00, a10, a01, a11: A
px0: a00 = a10
px1: a01 = a11
p0x: a00 = a01
p1x: a10 = a11
s: PathSquare px0 px1 p0x p1x
b00, b10, b01, b11: P
qx0: DPath (fun _ : A => P) px0 b00 b10
qx1: DPath (fun _ : A => P) px1 b01 b11
q0x: DPath (fun _ : A => P) p0x b00 b01
q1x: DPath (fun _ : A => P) p1x b10 b11
PathSquare (dp_const^-1 qx0) (dp_const^-1 qx1)
  (dp_const^-1 q0x) (dp_const^-1 q1x) <~>
DPathSquare (fun _ : A => P) s qx0 qx1 q0x q1x
  by destruct s.
Defined.

Notation ds_const' := equiv_ds_const'.

(** [dp_apD] fits into a natural square *)
Definition dp_apD_nat {A} {P : A -> Type} {f g : forall x, P x} {x y : A}
  (q : f == g) (p : x = y)
  : DPathSquare P (sq_refl_h _) (apD f p) (apD g p) (q x) (q y).A: Type
P: A -> Type
f, g: forall x : A, P x
x, y: A
q: f == g
p: x = y
DPathSquare P (sq_refl_h p) (apD f p) (apD g p) (q x)
  (q y)
Proof.A: Type
P: A -> Type
f, g: forall x : A, P x
x, y: A
q: f == g
p: x = y
DPathSquare P (sq_refl_h p) (apD f p) (apD g p) (q x)
  (q y)
  destruct p.A: Type
P: A -> Type
f, g: forall x : A, P x
x: A
q: f == g
DPathSquare P (sq_refl_h 1) (apD f 1) (apD g 1) (q x)
  (q x)
  by apply sq_1G.
Defined.

Definition equiv_ds_G1 {A} (P : A -> Type) {a00 a10 }
  {px0 px1 : a00 = a10} {p : px0 = px1} {b00 b10}
  (qx0 : DPath P px0 b00 b10) (qx1 : DPath P px1 b00 b10)
  : DPath (fun x => DPath P x b00 b10) p qx0 qx1
      <~> DPathSquare P (sq_G1 p) qx0 qx1 1 1.A: Type
P: A -> Type
a00, a10: A
px0, px1: a00 = a10
p: px0 = px1
b00: P a00
b10: P a10
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b00 b10
DPath (fun x : a00 = a10 => DPath P x b00 b10) p qx0
  qx1 <~> DPathSquare P (sq_G1 p) qx0 qx1 1 1
Proof.A: Type
P: A -> Type
a00, a10: A
px0, px1: a00 = a10
p: px0 = px1
b00: P a00
b10: P a10
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b00 b10
DPath (fun x : a00 = a10 => DPath P x b00 b10) p qx0
  qx1 <~> DPathSquare P (sq_G1 p) qx0 qx1 1 1
  destruct p, px0.A: Type
P: A -> Type
a00: A
b00, b10: P a00
qx0, qx1: DPath P 1 b00 b10
DPath (fun x : a00 = a00 => DPath P x b00 b10) 1 qx0
  qx1 <~> DPathSquare P (sq_G1 1%path) qx0 qx1 1 1
  exact sq_G1.
Defined.

Notation ds_G1 := equiv_ds_G1.

(** A [DPath] in a path-type is naturally a [DPathSquare].  *)

Definition equiv_ds_dp {A : Type} {B : A -> Type} (f g : forall a : A, B a)
  {x1 x2 : A} (p : x1 = x2) (q1 : f x1 = g x1) (q2 : f x2 = g x2)
  : DPath (fun x : A => f x = g x) p q1 q2
    <~> DPathSquare B (sq_refl_h p) (apD f p) (apD g p) q1 q2.A: Type
B: A -> Type
f, g: forall a : A, B a
x1, x2: A
p: x1 = x2
q1: f x1 = g x1
q2: f x2 = g x2
DPath (fun x : A => f x = g x) p q1 q2 <~>
DPathSquare B (sq_refl_h p) (apD f p) (apD g p) q1 q2
Proof.A: Type
B: A -> Type
f, g: forall a : A, B a
x1, x2: A
p: x1 = x2
q1: f x1 = g x1
q2: f x2 = g x2
DPath (fun x : A => f x = g x) p q1 q2 <~>
DPathSquare B (sq_refl_h p) (apD f p) (apD g p) q1 q2
  destruct p.A: Type
B: A -> Type
f, g: forall a : A, B a
x1: A
q1, q2: f x1 = g x1
DPath (fun x : A => f x = g x) 1 q1 q2 <~>
DPathSquare B (sq_refl_h 1) (apD f 1) (apD g 1) q1 q2
  exact sq_1G.
Defined.

Notation ds_dp := equiv_ds_dp.

(** Dependent Kan operations *)

Section Kan.

  Context {A : Type} {P : A -> Type} {a00 a10 a01 a11 : A}
          {px0 : a00 = a10} {px1 : a01 = a11} {p0x p1x}
          (s : PathSquare px0 px1 p0x p1x)
          {b00 : P a00} {b10 : P a10} {b01 : P a01} {b11 : P a11}.

  Definition ds_fill_l (qx1 : DPath P px1 b01 b11)
             (q0x : DPath P p0x b00 b01) (q1x : DPath P p1x b10 b11)
    : {qx0 : DPath P px0 b00 b10 & DPathSquare P s qx0 qx1 q0x q1x}.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
{qx0 : DPath P px0 b00 b10 &
DPathSquare P s qx0 qx1 q0x q1x}
  Proof.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
{qx0 : DPath P px0 b00 b10 &
DPathSquare P s qx0 qx1 q0x q1x}
    destruct s; apply sq_fill_l.
  Defined.

  Definition ds_fill_l_uniq {qx1 : DPath P px1 b01 b11}
             {q0x : DPath P p0x b00 b01} {q1x : DPath P p1x b10 b11}
             {qx0 : DPath P px0 b00 b10}
             (t : DPathSquare P s qx0 qx1 q0x q1x)
             {qx0' : DPath P px0 b00 b10}
             (t' : DPathSquare P s qx0' qx1 q0x q1x)
    : qx0 = qx0'.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
qx0: DPath P px0 b00 b10
t: DPathSquare P s qx0 qx1 q0x q1x
qx0': DPath P px0 b00 b10
t': DPathSquare P s qx0' qx1 q0x q1x
qx0 = qx0'
  Proof.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
qx0: DPath P px0 b00 b10
t: DPathSquare P s qx0 qx1 q0x q1x
qx0': DPath P px0 b00 b10
t': DPathSquare P s qx0' qx1 q0x q1x
qx0 = qx0'
    destruct s.A: Type
P: A -> Type
x: A
s: PathSquare 1 1 1 1
b00, b10, b01, b11: P x
qx1: DPath P 1 b01 b11
q0x: DPath P 1 b00 b01
q1x: DPath P 1 b10 b11
qx0: DPath P 1 b00 b10
t: DPathSquare P 1%square qx0 qx1 q0x q1x
qx0': DPath P 1 b00 b10
t': DPathSquare P 1%square qx0' qx1 q0x q1x
qx0 = qx0'
    exact (sq_fill_l_uniq t t').
  Defined.

  Definition ds_fill_r (qx0 : DPath P px0 b00 b10)
             (q0x : DPath P p0x b00 b01) (q1x : DPath P p1x b10 b11)
    : {qx1 : DPath P px1 b01 b11 & DPathSquare P s qx0 qx1 q0x q1x}.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
{qx1 : DPath P px1 b01 b11 &
DPathSquare P s qx0 qx1 q0x q1x}
  Proof.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
{qx1 : DPath P px1 b01 b11 &
DPathSquare P s qx0 qx1 q0x q1x}
    destruct s; apply sq_fill_r.
  Defined.

  Definition ds_fill_r_uniq {qx0 : DPath P px0 b00 b10}
             {q0x : DPath P p0x b00 b01} {q1x : DPath P p1x b10 b11}
             {qx1 : DPath P px1 b01 b11}
             (t : DPathSquare P s qx0 qx1 q0x q1x)
             {qx1' : DPath P px1 b01 b11}
             (t' : DPathSquare P s qx0 qx1' q0x q1x)
    : qx1 = qx1'.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
qx1: DPath P px1 b01 b11
t: DPathSquare P s qx0 qx1 q0x q1x
qx1': DPath P px1 b01 b11
t': DPathSquare P s qx0 qx1' q0x q1x
qx1 = qx1'
  Proof.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
qx1: DPath P px1 b01 b11
t: DPathSquare P s qx0 qx1 q0x q1x
qx1': DPath P px1 b01 b11
t': DPathSquare P s qx0 qx1' q0x q1x
qx1 = qx1'
    destruct s.A: Type
P: A -> Type
x: A
s: PathSquare 1 1 1 1
b00, b10, b01, b11: P x
qx0: DPath P 1 b00 b10
q0x: DPath P 1 b00 b01
q1x: DPath P 1 b10 b11
qx1: DPath P 1 b01 b11
t: DPathSquare P 1%square qx0 qx1 q0x q1x
qx1': DPath P 1 b01 b11
t': DPathSquare P 1%square qx0 qx1' q0x q1x
qx1 = qx1'
    exact (sq_fill_r_uniq t t').
  Defined.

  Definition equiv_ds_fill_lr
             {q0x : DPath P p0x b00 b01} {q1x : DPath P p1x b10 b11}
    : (DPath P px0 b00 b10) <~> (DPath P px1 b01 b11).A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
DPath P px0 b00 b10 <~> DPath P px1 b01 b11
  Proof.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
DPath P px0 b00 b10 <~> DPath P px1 b01 b11
    srapply equiv_adjointify.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
DPath P px0 b00 b10 -> DPath P px1 b01 b11
A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
DPath P px1 b01 b11 -> DPath P px0 b00 b10
A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
?f o ?g == idmap
A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
?g o ?f == idmap
    -A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
DPath P px0 b00 b10 -> DPath P px1 b01 b11 intros qx0; exact (ds_fill_r qx0 q0x q1x).1.
    -A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
DPath P px1 b01 b11 -> DPath P px0 b00 b10 intros qx1; exact (ds_fill_l qx1 q0x q1x).1.
    -A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
(fun qx0 : DPath P px0 b00 b10 =>
 (ds_fill_r qx0 q0x q1x).1)
o (fun qx1 : DPath P px1 b01 b11 =>
   (ds_fill_l qx1 q0x q1x).1) == idmap intros qx1.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
qx1: DPath P px1 b01 b11
(ds_fill_r (ds_fill_l qx1 q0x q1x).1 q0x q1x).1 = qx1
      exact (ds_fill_r_uniq (ds_fill_r _ q0x q1x).2
                            (ds_fill_l qx1 q0x q1x).2).
    -A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
(fun qx1 : DPath P px1 b01 b11 =>
 (ds_fill_l qx1 q0x q1x).1)
o (fun qx0 : DPath P px0 b00 b10 =>
   (ds_fill_r qx0 q0x q1x).1) == idmap intros qx0.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
q0x: DPath P p0x b00 b01
q1x: DPath P p1x b10 b11
qx0: DPath P px0 b00 b10
(ds_fill_l (ds_fill_r qx0 q0x q1x).1 q0x q1x).1 = qx0
      exact (ds_fill_l_uniq (ds_fill_l _ q0x q1x).2
                            (ds_fill_r qx0 q0x q1x).2).
  Defined.

  Definition ds_fill_t (qx0 : DPath P px0 b00 b10)
             (qx1 : DPath P px1 b01 b11) (q1x : DPath P p1x b10 b11)
    : {q0x : DPath P p0x b00 b01 & DPathSquare P s qx0 qx1 q0x q1x}.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b01 b11
q1x: DPath P p1x b10 b11
{q0x : DPath P p0x b00 b01 &
DPathSquare P s qx0 qx1 q0x q1x}
  Proof.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b01 b11
q1x: DPath P p1x b10 b11
{q0x : DPath P p0x b00 b01 &
DPathSquare P s qx0 qx1 q0x q1x}
    destruct s; apply sq_fill_t.
  Defined.

  Definition ds_fill_b (qx0 : DPath P px0 b00 b10)
             (qx1 : DPath P px1 b01 b11) (q0x : DPath P p0x b00 b01)
    : {q1x : DPath P p1x b10 b11 & DPathSquare P s qx0 qx1 q0x q1x}.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
{q1x : DPath P p1x b10 b11 &
DPathSquare P s qx0 qx1 q0x q1x}
  Proof.A: Type
P: 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
b00: P a00
b10: P a10
b01: P a01
b11: P a11
qx0: DPath P px0 b00 b10
qx1: DPath P px1 b01 b11
q0x: DPath P p0x b00 b01
{q1x : DPath P p1x b10 b11 &
DPathSquare P s qx0 qx1 q0x q1x}
    destruct s; apply sq_fill_b.
  Defined.

End Kan.

(** Another equivalent formulation of a dependent square over reflexivity *)
Definition equiv_ds_transport_dpath {A} {a0 a1 : A} {p : a0 = a1}
           {P : A -> Type} {b00 b10 b01 b11}
           (qx0 : DPath P p b00 b10) (qx1 : DPath P p b01 b11)
           (q0x : b00 = b01) (q1x : b10 = b11)
  : DPathSquare P (sq_refl_h p) qx0 qx1 q0x q1x
    <~> transport (fun y => DPath P p y b11) q0x
          (transport (fun y => DPath P p b00 y) q1x
                     qx0) = qx1.A: Type
a0, a1: A
p: a0 = a1
P: A -> Type
b00: P a0
b10: P a1
b01: P a0
b11: P a1
qx0: DPath P p b00 b10
qx1: DPath P p b01 b11
q0x: b00 = b01
q1x: b10 = b11
DPathSquare P (sq_refl_h p) qx0 qx1 q0x q1x <~>
transport (fun y : P a0 => DPath P p y b11) q0x
  (transport (fun y : P a1 => DPath P p b00 y) q1x qx0) =
qx1
Proof.A: Type
a0, a1: A
p: a0 = a1
P: A -> Type
b00: P a0
b10: P a1
b01: P a0
b11: P a1
qx0: DPath P p b00 b10
qx1: DPath P p b01 b11
q0x: b00 = b01
q1x: b10 = b11
DPathSquare P (sq_refl_h p) qx0 qx1 q0x q1x <~>
transport (fun y : P a0 => DPath P p y b11) q0x
  (transport (fun y : P a1 => DPath P p b00 y) q1x qx0) =
qx1
  destruct p; cbn.A: Type
a0: A
P: A -> Type
b00, b10, b01, b11: P a0
qx0: DPath P 1 b00 b10
qx1: DPath P 1 b01 b11
q0x: b00 = b01
q1x: b10 = b11
PathSquare qx0 qx1 q0x q1x <~>
transport (fun y : P a0 => y = b11) q0x
  (transport (fun y : P a0 => b00 = y) q1x qx0) = qx1
  refine (_ oE sq_path^-1).A: Type
a0: A
P: A -> Type
b00, b10, b01, b11: P a0
qx0: DPath P 1 b00 b10
qx1: DPath P 1 b01 b11
q0x: b00 = b01
q1x: b10 = b11
qx0 @ q1x = q0x @ qx1 <~>
transport (fun y : P a0 => y = b11) q0x
  (transport (fun y : P a0 => b00 = y) q1x qx0) = qx1
  refine (equiv_concat_l _ _ oE _).A: Type
a0: A
P: A -> Type
b00, b10, b01, b11: P a0
qx0: DPath P 1 b00 b10
qx1: DPath P 1 b01 b11
q0x: b00 = b01
q1x: b10 = b11
transport (fun y : P a0 => y = b11) q0x
  (transport (fun y : P a0 => b00 = y) q1x qx0) =
?Goal
A: Type
a0: A
P: A -> Type
b00, b10, b01, b11: P a0
qx0: DPath P 1 b00 b10
qx1: DPath P 1 b01 b11
q0x: b00 = b01
q1x: b10 = b11
qx0 @ q1x = q0x @ qx1 <~> ?Goal = qx1
  {A: Type
a0: A
P: A -> Type
b00, b10, b01, b11: P a0
qx0: DPath P 1 b00 b10
qx1: DPath P 1 b01 b11
q0x: b00 = b01
q1x: b10 = b11
transport (fun y : P a0 => y = b11) q0x
  (transport (fun y : P a0 => b00 = y) q1x qx0) =
?Goal apply transport_paths_l. }A: Type
a0: A
P: A -> Type
b00, b10, b01, b11: P a0
qx0: DPath P 1 b00 b10
qx1: DPath P 1 b01 b11
q0x: b00 = b01
q1x: b10 = b11
qx0 @ q1x = q0x @ qx1 <~>
q0x^ @ transport (fun y : P a0 => b00 = y) q1x qx0 =
qx1
  refine (equiv_moveR_Vp _ _ _ oE _).A: Type
a0: A
P: A -> Type
b00, b10, b01, b11: P a0
qx0: DPath P 1 b00 b10
qx1: DPath P 1 b01 b11
q0x: b00 = b01
q1x: b10 = b11
qx0 @ q1x = q0x @ qx1 <~>
transport (fun y : P a0 => b00 = y) q1x qx0 =
q0x @ qx1
  refine (equiv_concat_l _ _).A: Type
a0: A
P: A -> Type
b00, b10, b01, b11: P a0
qx0: DPath P 1 b00 b10
qx1: DPath P 1 b01 b11
q0x: b00 = b01
q1x: b10 = b11
transport (fun y : P a0 => b00 = y) q1x qx0 =
qx0 @ q1x
  apply transport_paths_r.
Defined.

Notation ds_transport_dpath := equiv_ds_transport_dpath.