DPath.v

Require Import Basics.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Paths Types.Sigma Types.Forall.

Declare Scope dpath_scope.
Delimit Scope dpath_scope with dpath.

Local Open Scope dpath_scope.

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

(** This allows DPaths to collapse to paths under cbn *)
Arguments DPath _ / _ _ _ : simpl nomatch.

Global Instance istrunc_dp {A : Type} {P : A -> Type} {n : trunc_index}
 {a0 a1} {p : a0 = a1} {b0 : P a0} {b1 : P a1} `{IsTrunc n.+1 (P a0)}
  `{IsTrunc n.+1 (P a1)} : IsTrunc n (DPath P p b0 b1) := _.

Definition dp_ishprop {A : Type} (P : A -> Type) {a0 a1} {p : a0 = a1}
  {b0 : P a0} {b1 : P a1} `{IsHProp (P a0)} `{IsHProp (P a1)}
  : DPath P p b0 b1.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
IsHProp0: IsHProp (P a0)
IsHProp1: IsHProp (P a1)
DPath P p b0 b1
Proof.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
IsHProp0: IsHProp (P a0)
IsHProp1: IsHProp (P a1)
DPath P p b0 b1
  apply path_ishprop.
Defined.

(** We have reflexivity for DPaths, this helps coq guess later *)
Definition dp_id {A} {P : A -> Type} {a : A} {x : P a} : DPath P 1 x x := 1%path.

(** Although [1%dpath] is definitionally [1%path], when [1%path] is used where a dependent path is expected, Coq sometimes has trouble interpreting this. So we make a custom notation for [1] in [dpath_scope]. *)
Notation "1" := dp_id : dpath_scope.

(** DPath induction *)
Definition DPath_ind (A : Type) (P : A -> Type) (P0 : forall (a0 a1 : A)
  (p : a0 = a1) (b0 : P a0) (b1 : P a1), DPath P p b0 b1 -> Type)
  : (forall (x : A) (y : P x), P0 x x 1%path y y 1) ->
    forall (a0 a1 : A) (p : a0 = a1) (b0 : P a0) (b1 : P a1)
    (d : DPath P p b0 b1), P0 a0 a1 p b0 b1 d.A: Type
P: A -> Type
P0: forall (a0 a1 : A) (p : a0 = a1) (b0 : P a0)
(b1 : P a1), DPath P p b0 b1 -> Type
(forall (x : A) (y : P x), P0 x x 1%path y y 1) ->
forall (a0 a1 : A) (p : a0 = a1) (b0 : P a0)
(b1 : P a1) (d : DPath P p b0 b1), P0 a0 a1 p b0 b1 d
Proof.A: Type
P: A -> Type
P0: forall (a0 a1 : A) (p : a0 = a1) (b0 : P a0)
(b1 : P a1), DPath P p b0 b1 -> Type
(forall (x : A) (y : P x), P0 x x 1%path y y 1) ->
forall (a0 a1 : A) (p : a0 = a1) (b0 : P a0)
(b1 : P a1) (d : DPath P p b0 b1), P0 a0 a1 p b0 b1 d
  intros X a0 a1 [] b0 b1 []; apply X.
Defined.

(** A DPath over a constant family is just a path *)
Definition equiv_dp_const {A C} {a0 a1 : A} {p : a0 = a1} {x y}
  : (x = y) <~> DPath (fun _ => C) p x y.A, C: Type
a0, a1: A
p: a0 = a1
x, y: C
x = y <~> DPath (fun _ : A => C) p x y
Proof.A, C: Type
a0, a1: A
p: a0 = a1
x, y: C
x = y <~> DPath (fun _ : A => C) p x y
  by destruct p.
Defined.

Notation dp_const := equiv_dp_const.

(** dp_apD of a non-dependent map is just a constant DPath *)
Definition dp_apD_const {A B} (f : A -> B) {a0 a1 : A}
  (p : a0 = a1) : apD f p = dp_const (ap f p).A, B: Type
f: A -> B
a0, a1: A
p: a0 = a1
apD f p = dp_const (ap f p)
Proof.A, B: Type
f: A -> B
a0, a1: A
p: a0 = a1
apD f p = dp_const (ap f p)
  by destruct p.
Defined.

(** An alternate version useful for proving recursion computation rules from induction ones *)
Definition dp_apD_const' {A B : Type} {f : A -> B} {a0 a1 : A}
  {p : a0 = a1} : dp_const^-1 (apD f p) = ap f p.A, B: Type
f: A -> B
a0, a1: A
p: a0 = a1
dp_const^-1 (apD f p) = ap f p
Proof.A, B: Type
f: A -> B
a0, a1: A
p: a0 = a1
dp_const^-1 (apD f p) = ap f p
  apply moveR_equiv_V.A, B: Type
f: A -> B
a0, a1: A
p: a0 = a1
apD f p = dp_const (ap f p)
  apply dp_apD_const.
Defined.

(** Concatenation of dependent paths *)
Definition dp_concat {A} {P : A -> Type} {a0 a1 a2}
  {p : a0 = a1} {q : a1 = a2} {b0 : P a0} {b1 : P a1} {b2 : P a2}
  : DPath P p b0 b1 -> DPath P q b1 b2 -> DPath P (p @ q) b0 b2.A: Type
P: A -> Type
a0, a1, a2: A
p: a0 = a1
q: a1 = a2
b0: P a0
b1: P a1
b2: P a2
DPath P p b0 b1 ->
DPath P q b1 b2 -> DPath P (p @ q) b0 b2
Proof.A: Type
P: A -> Type
a0, a1, a2: A
p: a0 = a1
q: a1 = a2
b0: P a0
b1: P a1
b2: P a2
DPath P p b0 b1 ->
DPath P q b1 b2 -> DPath P (p @ q) b0 b2
  destruct p, q.A: Type
P: A -> Type
a0: A
b0, b1, b2: P a0
DPath P 1 b0 b1 ->
DPath P 1 b1 b2 -> DPath P (1 @ 1) b0 b2
  exact concat.
Defined.

Notation "x '@Dp' y" := (dp_concat x y) : dpath_scope.

(** Concatenation of dependent paths with non-dependent paths *)
Definition dp_concat_r {A} {P : A -> Type} {a0 a1}
  {p : a0 = a1} {b0 : P a0} {b1 b2 : P a1}
  : DPath P p b0 b1 -> (b1 = b2) -> DPath P p b0 b2.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1, b2: P a1
DPath P p b0 b1 -> b1 = b2 -> DPath P p b0 b2
Proof.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1, b2: P a1
DPath P p b0 b1 -> b1 = b2 -> DPath P p b0 b2
  destruct p; exact concat.
Defined.

Notation "x '@Dr' y" := (dp_concat_r x y) : dpath_scope.

Definition dp_concat_l {A} {P : A -> Type} {a1 a2}
  {q : a1 = a2} {b0 b1 : P a1} {b2 : P a2}
  : (b0 = b1) -> DPath P q b1 b2 -> DPath P q b0 b2.A: Type
P: A -> Type
a1, a2: A
q: a1 = a2
b0, b1: P a1
b2: P a2
b0 = b1 -> DPath P q b1 b2 -> DPath P q b0 b2
Proof.A: Type
P: A -> Type
a1, a2: A
q: a1 = a2
b0, b1: P a1
b2: P a2
b0 = b1 -> DPath P q b1 b2 -> DPath P q b0 b2
  destruct q; exact concat.
Defined.

Notation "x '@Dl' y" := (dp_concat_l x y) : dpath_scope.

(** Inverse of dependent paths *)
Definition dp_inverse {A} {P : A -> Type} {a0 a1} {p : a0 = a1}
  {b0 : P a0} {b1 : P a1} : DPath P p b0 b1 -> DPath P p^ b1 b0.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
DPath P p b0 b1 -> DPath P p^ b1 b0
Proof.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
DPath P p b0 b1 -> DPath P p^ b1 b0
  destruct p.A: Type
P: A -> Type
a0: A
b0, b1: P a0
DPath P 1 b0 b1 -> DPath P 1^ b1 b0
  exact inverse.
Defined.

Notation "x '^D'" := (dp_inverse x) : dpath_scope.

(** dp_apD distributes over concatenation *)
Definition dp_apD_pp (A : Type) (P : A -> Type) (f : forall a, P a)
  {a0 a1 a2 : A} (p : a0 = a1) (q : a1 = a2)
  : apD f (p @ q) = (apD f p) @Dp (apD f q).A: Type
P: A -> Type
f: forall a : A, P a
a0, a1, a2: A
p: a0 = a1
q: a1 = a2
apD f (p @ q) = apD f p @Dp apD f q
Proof.A: Type
P: A -> Type
f: forall a : A, P a
a0, a1, a2: A
p: a0 = a1
q: a1 = a2
apD f (p @ q) = apD f p @Dp apD f q
  by destruct p, q.
Defined.

(** dp_apD respects inverses *)
Definition dp_apD_V (A : Type) (P : A -> Type) (f : forall a, P a)
  {a0 a1 : A} (p : a0 = a1) : apD f p^ = (apD f p)^D.A: Type
P: A -> Type
f: forall a : A, P a
a0, a1: A
p: a0 = a1
apD f p^ = (apD f p) ^D
Proof.A: Type
P: A -> Type
f: forall a : A, P a
a0, a1: A
p: a0 = a1
apD f p^ = (apD f p) ^D
  by destruct p.
Defined.

(** [dp_const] preserves concatenation *)
Definition dp_const_pp {A B : Type} {a0 a1 a2 : A}
  {p : a0 = a1} {q : a1 = a2} {x y z : B} (r : x = y) (s : y = z)
  : dp_const (p:=p @ q) (r @ s) = (dp_const (p:=p) r) @Dp (dp_const (p:=q) s).A, B: Type
a0, a1, a2: A
p: a0 = a1
q: a1 = a2
x, y, z: B
r: x = y
s: y = z
dp_const (r @ s) = dp_const r @Dp dp_const s
Proof.A, B: Type
a0, a1, a2: A
p: a0 = a1
q: a1 = a2
x, y, z: B
r: x = y
s: y = z
dp_const (r @ s) = dp_const r @Dp dp_const s
  by destruct p,q.
Defined.

(** [dp_const] preserves inverses *) 
Definition dp_const_V {A B : Type} {a0 a1 : A} {p : a0 = a1} {x y : B} (r : x = y)
  : dp_const r^ = (dp_const (p:=p) r)^D.A, B: Type
a0, a1: A
p: a0 = a1
x, y: B
r: x = y
dp_const r^ = (dp_const r) ^D
Proof.A, B: Type
a0, a1: A
p: a0 = a1
x, y: B
r: x = y
dp_const r^ = (dp_const r) ^D
  by destruct p.
Defined. 

Section DGroupoid.

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

  Definition dp_concat_p1
    : DPath (fun t : a0 = a1 => DPath P t b0 b1) (concat_p1 p) (dp @Dp 1) dp.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
dp: DPath P p b0 b1
DPath (fun t : a0 = a1 => DPath P t b0 b1)
  (concat_p1 p) (dp @Dp 1) dp
  Proof.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
dp: DPath P p b0 b1
DPath (fun t : a0 = a1 => DPath P t b0 b1)
  (concat_p1 p) (dp @Dp 1) dp
    destruct p.A: Type
P: A -> Type
a0: A
p: a0 = a0
b0, b1: P a0
dp: DPath P 1 b0 b1
DPath (fun t : a0 = a0 => DPath P t b0 b1)
  (concat_p1 1) (dp @Dp 1) dp
    apply concat_p1.
  Defined.

  Definition dp_concat_1p
    : DPath (fun t : a0 = a1 => DPath P t b0 b1) (concat_1p p) (1 @Dp dp) dp.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
dp: DPath P p b0 b1
DPath (fun t : a0 = a1 => DPath P t b0 b1)
  (concat_1p p) (1 @Dp dp) dp
  Proof.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
dp: DPath P p b0 b1
DPath (fun t : a0 = a1 => DPath P t b0 b1)
  (concat_1p p) (1 @Dp dp) dp
    destruct p.A: Type
P: A -> Type
a0: A
p: a0 = a0
b0, b1: P a0
dp: DPath P 1 b0 b1
DPath (fun t : a0 = a0 => DPath P t b0 b1)
  (concat_1p 1) (1 @Dp dp) dp
    apply concat_1p.
  Defined.

  Definition dp_concat_Vp
    : DPath (fun t : a1 = a1 => DPath P t b1 b1) (concat_Vp p) (dp^D @Dp dp) 1.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
dp: DPath P p b0 b1
DPath (fun t : a1 = a1 => DPath P t b1 b1)
  (concat_Vp p) (dp ^D @Dp dp) 1
  Proof.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
dp: DPath P p b0 b1
DPath (fun t : a1 = a1 => DPath P t b1 b1)
  (concat_Vp p) (dp ^D @Dp dp) 1
    destruct p.A: Type
P: A -> Type
a0: A
p: a0 = a0
b0, b1: P a0
dp: DPath P 1 b0 b1
DPath (fun t : a0 = a0 => DPath P t b1 b1)
  (concat_Vp 1) (dp ^D @Dp dp) 1
    apply concat_Vp.
  Defined.

  Definition dp_concat_pV
    : DPath (fun t : a0 = a0 => DPath P t b0 b0) (concat_pV p) (dp @Dp dp^D) 1.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
dp: DPath P p b0 b1
DPath (fun t : a0 = a0 => DPath P t b0 b0)
  (concat_pV p) (dp @Dp dp ^D) 1
  Proof.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
dp: DPath P p b0 b1
DPath (fun t : a0 = a0 => DPath P t b0 b0)
  (concat_pV p) (dp @Dp dp ^D) 1
    destruct p.A: Type
P: A -> Type
a0: A
p: a0 = a0
b0, b1: P a0
dp: DPath P 1 b0 b1
DPath (fun t : a0 = a0 => DPath P t b0 b0)
  (concat_pV 1) (dp @Dp dp ^D) 1
    apply concat_pV.
  Defined.

  Section Concat.

    Context {a2 a3} {q : a1 = a2} {r : a2 = a3}
       {b2 : P a2} {b3 : P a3}
       (dq : DPath P q b1 b2) (dr : DPath P  r b2 b3).

    Definition dp_concat_pp_p
      : DPath (fun t : a0 = a3 => DPath P t b0 b3) (concat_pp_p p q r)
        ((dp @Dp dq) @Dp dr) (dp @Dp (dq @Dp dr)).A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
dp: DPath P p b0 b1
a2, a3: A
q: a1 = a2
r: a2 = a3
b2: P a2
b3: P a3
dq: DPath P q b1 b2
dr: DPath P r b2 b3
DPath (fun t : a0 = a3 => DPath P t b0 b3)
  (concat_pp_p p q r) ((dp @Dp dq) @Dp dr)
  (dp @Dp (dq @Dp dr))
    Proof.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
dp: DPath P p b0 b1
a2, a3: A
q: a1 = a2
r: a2 = a3
b2: P a2
b3: P a3
dq: DPath P q b1 b2
dr: DPath P r b2 b3
DPath (fun t : a0 = a3 => DPath P t b0 b3)
  (concat_pp_p p q r) ((dp @Dp dq) @Dp dr)
  (dp @Dp (dq @Dp dr))
      destruct p, q, r.A: Type
P: A -> Type
a0: A
p: a0 = a0
b0, b1: P a0
dp: DPath P 1 b0 b1
q, r: a0 = a0
b2, b3: P a0
dq: DPath P 1 b1 b2
dr: DPath P 1 b2 b3
DPath (fun t : a0 = a0 => DPath P t b0 b3)
  (concat_pp_p 1 1 1) ((dp @Dp dq) @Dp dr)
  (dp @Dp (dq @Dp dr))
      apply concat_pp_p.
    Defined.

    Definition dp_concat_p_pp
      : DPath (fun t : a0 = a3 => DPath P t b0 b3) (concat_p_pp p q r)
        (dp @Dp (dq @Dp dr)) ((dp @Dp dq) @Dp dr).A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
dp: DPath P p b0 b1
a2, a3: A
q: a1 = a2
r: a2 = a3
b2: P a2
b3: P a3
dq: DPath P q b1 b2
dr: DPath P r b2 b3
DPath (fun t : a0 = a3 => DPath P t b0 b3)
  (concat_p_pp p q r) (dp @Dp (dq @Dp dr))
  ((dp @Dp dq) @Dp dr)
    Proof.A: Type
P: A -> Type
a0, a1: A
p: a0 = a1
b0: P a0
b1: P a1
dp: DPath P p b0 b1
a2, a3: A
q: a1 = a2
r: a2 = a3
b2: P a2
b3: P a3
dq: DPath P q b1 b2
dr: DPath P r b2 b3
DPath (fun t : a0 = a3 => DPath P t b0 b3)
  (concat_p_pp p q r) (dp @Dp (dq @Dp dr))
  ((dp @Dp dq) @Dp dr)
      destruct p, q, r.A: Type
P: A -> Type
a0: A
p: a0 = a0
b0, b1: P a0
dp: DPath P 1 b0 b1
q, r: a0 = a0
b2, b3: P a0
dq: DPath P 1 b1 b2
dr: DPath P 1 b2 b3
DPath (fun t : a0 = a0 => DPath P t b0 b3)
  (concat_p_pp 1 1 1) (dp @Dp (dq @Dp dr))
  ((dp @Dp dq) @Dp dr)
      apply concat_p_pp.
    Defined.

  End Concat.

End DGroupoid.

(** Dependent paths over paths *)
(** These can be found under names such as dp_paths_l akin to transport_paths_l *)

Definition equiv_dp_paths_l {A : Type} {x1 x2 y : A} (p : x1 = x2) (q : x1 = y) r
  : p^ @ q = r <~> DPath (fun x => x = y) p q r.A: Type
x1, x2, y: A
p: x1 = x2
q: x1 = y
r: x2 = y
p^ @ q = r <~> DPath (fun x : A => x = y) p q r
Proof.A: Type
x1, x2, y: A
p: x1 = x2
q: x1 = y
r: x2 = y
p^ @ q = r <~> DPath (fun x : A => x = y) p q r
  apply equiv_concat_l, transport_paths_l.
Defined.

Notation dp_paths_l := equiv_dp_paths_l.

Definition equiv_dp_paths_r {A : Type} {x y1 y2 : A} (p : y1 = y2) (q : x = y1) r
  :  q @ p = r <~> DPath (fun y => x = y) p q r.A: Type
x, y1, y2: A
p: y1 = y2
q: x = y1
r: x = y2
q @ p = r <~> DPath (fun y : A => x = y) p q r
Proof.A: Type
x, y1, y2: A
p: y1 = y2
q: x = y1
r: x = y2
q @ p = r <~> DPath (fun y : A => x = y) p q r
  apply equiv_concat_l, transport_paths_r.
Defined.

Notation dp_paths_r := equiv_dp_paths_r.

Definition equiv_dp_paths_lr {A : Type} {x1 x2 : A} (p : x1 = x2) (q : x1 = x1) r
  : (p^ @ q) @ p = r <~> DPath (fun x : A => x = x) p q r.A: Type
x1, x2: A
p: x1 = x2
q: x1 = x1
r: x2 = x2
(p^ @ q) @ p = r <~> DPath (fun x : A => x = x) p q r
Proof.A: Type
x1, x2: A
p: x1 = x2
q: x1 = x1
r: x2 = x2
(p^ @ q) @ p = r <~> DPath (fun x : A => x = x) p q r
  apply equiv_concat_l, transport_paths_lr.
Defined.

Notation dp_paths_lr := equiv_dp_paths_lr.

Definition equiv_dp_paths_Fl {A B} {f : A -> B} {x1 x2 : A} {y : B} (p : x1 = x2)
  (q : f x1 = y) r :  (ap f p)^ @ q = r <~> DPath (fun x => f x = y) p q r.A, B: Type
f: A -> B
x1, x2: A
y: B
p: x1 = x2
q: f x1 = y
r: f x2 = y
(ap f p)^ @ q = r <~>
DPath (fun x : A => f x = y) p q r
Proof.A, B: Type
f: A -> B
x1, x2: A
y: B
p: x1 = x2
q: f x1 = y
r: f x2 = y
(ap f p)^ @ q = r <~>
DPath (fun x : A => f x = y) p q r
  apply equiv_concat_l, transport_paths_Fl.
Defined.

Notation dp_paths_Fl := equiv_dp_paths_Fl.

Definition equiv_dp_paths_Fr {A B} {g : A -> B} {y1 y2 : A} {x : B} (p : y1 = y2)
  (q : x = g y1) r :  q @ ap g p = r <~> DPath (fun y : A => x = g y) p q r.A, B: Type
g: A -> B
y1, y2: A
x: B
p: y1 = y2
q: x = g y1
r: x = g y2
q @ ap g p = r <~> DPath (fun y : A => x = g y) p q r
Proof.A, B: Type
g: A -> B
y1, y2: A
x: B
p: y1 = y2
q: x = g y1
r: x = g y2
q @ ap g p = r <~> DPath (fun y : A => x = g y) p q r
  apply equiv_concat_l, transport_paths_Fr.
Defined.

Notation dp_paths_Fr := equiv_dp_paths_Fr.

Definition equiv_dp_paths_FFlr {A B} {f : A -> B} {g : B -> A} {x1 x2 : A}
  (p : x1 = x2) (q : g (f x1) = x1) r
  : ((ap g (ap f p))^ @ q) @ p = r <~> DPath (fun x : A => g (f x) = x) p q r.A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: g (f x1) = x1
r: g (f x2) = x2
((ap g (ap f p))^ @ q) @ p = r <~>
DPath (fun x : A => g (f x) = x) p q r
Proof.A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: g (f x1) = x1
r: g (f x2) = x2
((ap g (ap f p))^ @ q) @ p = r <~>
DPath (fun x : A => g (f x) = x) p q r
  apply equiv_concat_l, transport_paths_FFlr.
Defined.

Notation dp_paths_FFlr := equiv_dp_paths_FFlr.

Definition equiv_dp_paths_FlFr {A B} {f g : A -> B} {x1 x2 : A} (p : x1 = x2)
  (q : f x1 = g x1) r
  : ((ap f p)^ @ q) @ ap g p = r <~> DPath (fun x : A => f x = g x) p q r.A, B: Type
f, g: A -> B
x1, x2: A
p: x1 = x2
q: f x1 = g x1
r: f x2 = g x2
((ap f p)^ @ q) @ ap g p = r <~>
DPath (fun x : A => f x = g x) p q r
Proof.A, B: Type
f, g: A -> B
x1, x2: A
p: x1 = x2
q: f x1 = g x1
r: f x2 = g x2
((ap f p)^ @ q) @ ap g p = r <~>
DPath (fun x : A => f x = g x) p q r
  apply equiv_concat_l, transport_paths_FlFr.
Defined.

Notation dp_paths_FlFr := equiv_dp_paths_FlFr.

Definition equiv_dp_paths_lFFr {A B} {f : A -> B} {g : B -> A} {x1 x2 : A} 
  (p : x1 = x2) (q : x1 = g (f x1)) r
  :  (p^ @ q) @ ap g (ap f p) = r <~> DPath (fun x : A => x = g (f x)) p q r.A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: x1 = g (f x1)
r: x2 = g (f x2)
(p^ @ q) @ ap g (ap f p) = r <~>
DPath (fun x : A => x = g (f x)) p q r
Proof.A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: x1 = g (f x1)
r: x2 = g (f x2)
(p^ @ q) @ ap g (ap f p) = r <~>
DPath (fun x : A => x = g (f x)) p q r
  apply equiv_concat_l, transport_paths_lFFr.
Defined.

Notation dp_paths_lFFr := equiv_dp_paths_lFFr.

Definition equiv_dp_paths_FlFr_D {A B} (f g : forall a : A, B a) 
  {x1 x2 : A} (p : x1 = x2) (q : f x1 = g x1) (r : f x2 = g x2)
  : ((apD f p)^ @ ap (transport B p) q) @ apD g p = r
    <~> DPath (fun x : A => f x = g x) p q r.A: Type
B: A -> Type
f, g: forall a : A, B a
x1, x2: A
p: x1 = x2
q: f x1 = g x1
r: f x2 = g x2
((apD f p)^ @ ap (transport B p) q) @ apD g p = r <~>
DPath (fun x : A => f x = g x) p q r
Proof.A: Type
B: A -> Type
f, g: forall a : A, B a
x1, x2: A
p: x1 = x2
q: f x1 = g x1
r: f x2 = g x2
((apD f p)^ @ ap (transport B p) q) @ apD g p = r <~>
DPath (fun x : A => f x = g x) p q r
  apply equiv_concat_l, transport_paths_FlFr_D.
Defined.

Notation dp_paths_FlFr_D := equiv_dp_paths_FlFr_D.

Definition equiv_dp_compose' {A B} (f : A -> B) (P : B -> Type) {x y : A}
  {p : x = y} {q : f x = f y} (r : ap f p = q) {u : P (f x)} {v : P (f y)}
  : DPath (fun x => P (f x)) p u v <~> DPath P q u v.A, B: Type
f: A -> B
P: B -> Type
x, y: A
p: x = y
q: f x = f y
r: ap f p = q
u: P (f x)
v: P (f y)
DPath (fun x : A => P (f x)) p u v <~> DPath P q u v
Proof.A, B: Type
f: A -> B
P: B -> Type
x, y: A
p: x = y
q: f x = f y
r: ap f p = q
u: P (f x)
v: P (f y)
DPath (fun x : A => P (f x)) p u v <~> DPath P q u v
  by destruct r, p.
Defined.

Notation dp_compose' := equiv_dp_compose'.

Definition equiv_dp_compose {A B} (f : A -> B) (P : B -> Type) {x y : A}
  (p : x = y) {u : P (f x)} {v : P (f y)}
  : DPath (fun x => P (f x)) p u v <~> DPath P (ap f p) u v
  := dp_compose' f P (idpath (ap f p)).

Notation dp_compose := equiv_dp_compose.

Definition dp_apD_compose' {A B : Type} (f : A -> B) (P : B -> Type)
           {x y : A} {p : x = y} {q : f x = f y} (r : ap f p = q) (g : forall b:B, P b)
  : apD (g o f) p = (dp_compose' f P r)^-1 (apD g q).A, B: Type
f: A -> B
P: B -> Type
x, y: A
p: x = y
q: f x = f y
r: ap f p = q
g: forall b : B, P b
apD (g o f) p = (dp_compose' f P r)^-1 (apD g q)
Proof.A, B: Type
f: A -> B
P: B -> Type
x, y: A
p: x = y
q: f x = f y
r: ap f p = q
g: forall b : B, P b
apD (g o f) p = (dp_compose' f P r)^-1 (apD g q)
  by destruct r, p.
Defined.

Definition dp_apD_compose {A B : Type} (f : A -> B) (P : B -> Type)
           {x y : A} (p : x = y) (g : forall b:B, P b)
  : apD (g o f) p = (dp_compose f P p)^-1 (apD g (ap f p))
  := dp_apD_compose' f P (idpath (ap f p)) g.

(** Type constructors *)

(** Many of these lemmas exist already for transports but we prove them for
   DPaths anyway. If we change the definition of DPath to the transport,
   then these will no longer be needed. It is however, far more readable
   to keep such lemmas seperate, since it is difficult to otherwise search
   for a DPath lemma if they are all written using transports. *)

(** A version of [equiv_path_sigma] for [DPath]s *)
Definition equiv_path_sigma_dp {A P} {x x' : A} {y : P x} {y' : P x'}
  : {p : x = x' & DPath P p y y'} <~> (x; y) = (x'; y')
  := equiv_path_sigma P (x; y) (x'; y').

Notation path_sigma_dp := equiv_path_sigma_dp.

Definition ap_pr1_path_sigma_dp {A : Type} {P : A -> Type}
  {x x' : A} {y : P x} {y' : P x'} (p : x = x') (q : DPath P p y y')
  : ap pr1 (path_sigma_dp (p; q)) = p.A: Type
P: A -> Type
x, x': A
y: P x
y': P x'
p: x = x'
q: DPath P p y y'
ap pr1 (path_sigma_dp (p; q)) = p
Proof.A: Type
P: A -> Type
x, x': A
y: P x
y': P x'
p: x = x'
q: DPath P p y y'
ap pr1 (path_sigma_dp (p; q)) = p
  apply ap_pr1_path_sigma.
Defined.

(* DPath over a forall *)
Definition equiv_dp_forall `{Funext} {A : Type} {B : A -> Type} {C : sig B -> Type}
  {a1 a2 : A} {p : a1 = a2} {f : forall x, C (a1; x)} {g : forall x, C (a2; x)}
  : (forall (x : B a1) (y : B a2) (q : DPath B p x y),
    DPath C (path_sigma_dp (p; q)) (f x) (g y))
    <~> DPath (fun a => forall x, C (a; x)) p f g.H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1, a2: A
p: a1 = a2
f: forall x : B a1, C (a1; x)
g: forall x : B a2, C (a2; x)
(forall (x : B a1) (y : B a2) (q : DPath B p x y),
 DPath C (path_sigma_dp (p; q)) (f x) (g y)) <~>
DPath (fun a : A => forall x : B a, C (a; x)) p f g
Proof.H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1, a2: A
p: a1 = a2
f: forall x : B a1, C (a1; x)
g: forall x : B a2, C (a2; x)
(forall (x : B a1) (y : B a2) (q : DPath B p x y),
 DPath C (path_sigma_dp (p; q)) (f x) (g y)) <~>
DPath (fun a : A => forall x : B a, C (a; x)) p f g
  symmetry.H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1, a2: A
p: a1 = a2
f: forall x : B a1, C (a1; x)
g: forall x : B a2, C (a2; x)
DPath (fun a : A => forall x : B a, C (a; x)) p f g <~>
(forall (x : B a1) (y : B a2) (q : DPath B p x y),
 DPath C (path_sigma_dp (p; q)) (f x) (g y))
  destruct p; cbn.H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
f = g <~>
(forall (x y : B a1) (q : x = y),
 transport C
   (path_sigma_uncurried B (a1; x) (a1; y) (1%path; q))
   (f x) = g y)
  refine (equiv_compose' _ (equiv_apD10 _ _ _)).H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
f == g <~>
(forall (x y : B a1) (q : x = y),
 transport C
   (path_sigma_uncurried B (a1; x) (a1; y) (1%path; q))
   (f x) = g y)
  apply equiv_functor_forall_id.H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
forall a : B a1,
f a = g a <~>
(forall (y : B a1) (q : a = y),
 transport C
   (path_sigma_uncurried B (a1; a) (a1; y) (1%path; q))
   (f a) = g y)
  intro a.H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
a: B a1
f a = g a <~>
(forall (y : B a1) (q : a = y),
 transport C
   (path_sigma_uncurried B (a1; a) (a1; y) (1%path; q))
   (f a) = g y)
  srapply equiv_adjointify.H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
a: B a1
f a = g a ->
forall (y : B a1) (q : a = y),
transport C
  (path_sigma_uncurried B (a1; a) (a1; y) (1%path; q))
  (f a) = g y
H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
a: B a1
(forall (y : B a1) (q : a = y),
 transport C
   (path_sigma_uncurried B (a1; a) (a1; y) (1%path; q))
   (f a) = g y) -> f a = g a
H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
a: B a1
?f o ?g == idmap
H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
a: B a1
?g o ?f == idmap
  +H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
a: B a1
f a = g a ->
forall (y : B a1) (q : a = y),
transport C
  (path_sigma_uncurried B (a1; a) (a1; y) (1%path; q))
  (f a) = g y by intros ? ? [].
  +H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
a: B a1
(forall (y : B a1) (q : a = y),
 transport C
   (path_sigma_uncurried B (a1; a) (a1; y) (1%path; q))
   (f a) = g y) -> f a = g a intro F; exact (F a 1).
  +H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
a: B a1
(fun (X : f a = g a) (y : B a1) (q : a = y) =>
 match
   q as p in (_ = b)
   return
     (transport C
        (path_sigma_uncurried B (a1; a) (a1; b)
           (1%path; p)) (f a) = g b)
 with
 | 1%path => X
 end)
o (fun
     F : forall (y : B a1) (q : a = y),
         transport C
           (path_sigma_uncurried B (a1; a) (a1; y)
              (1%path; q)) (f a) = g y => F a 1) ==
idmap repeat (intro; apply path_forall).H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
a: B a1
x: forall (y : B a1) (q : a = y),
transport C
  (path_sigma_uncurried B (a1; a) (a1; y)
     (1%path; q)) (f a) = g y
x0: B a1
(fun q : a = x0 =>
 match
   q as p in (_ = b)
   return
     (transport C
        (path_sigma_uncurried B (a1; a) (a1; b)
           (1%path; p)) (f a) = g b)
 with
 | 1%path => x a 1
 end) == x x0
    by intros [].
  +H: Funext
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
a1: A
f, g: forall x : B a1, C (a1; x)
a: B a1
(fun
   F : forall (y : B a1) (q : a = y),
       transport C
         (path_sigma_uncurried B (a1; a) (a1; y)
            (1%path; q)) (f a) = g y => F a 1)
o (fun (X : f a = g a) (y : B a1) (q : a = y) =>
   match
     q as p in (_ = b)
     return
       (transport C
          (path_sigma_uncurried B (a1; a) (a1; b)
             (1%path; p)) (f a) = g b)
   with
   | 1%path => X
   end) == idmap by intro.
Defined.

Notation dp_forall := equiv_dp_forall.

(* DPath over an arrow *)
Definition equiv_dp_arrow `{Funext} {A : Type} {B C : A -> Type}
  {a1 a2 : A} {p : a1 = a2} {f :  B a1 -> C a1} {g : B a2 -> C a2}
  : (forall x, DPath C p (f x) (g (p # x)))
    <~> DPath (fun x => B x -> C x) p f g.H: Funext
A: Type
B, C: A -> Type
a1, a2: A
p: a1 = a2
f: B a1 -> C a1
g: B a2 -> C a2
(forall x : B a1,
 DPath C p (f x) (g (transport B p x))) <~>
DPath (fun x : A => B x -> C x) p f g
Proof.H: Funext
A: Type
B, C: A -> Type
a1, a2: A
p: a1 = a2
f: B a1 -> C a1
g: B a2 -> C a2
(forall x : B a1,
 DPath C p (f x) (g (transport B p x))) <~>
DPath (fun x : A => B x -> C x) p f g
  destruct p.H: Funext
A: Type
B, C: A -> Type
a1: A
f, g: B a1 -> C a1
(forall x : B a1,
 DPath C 1 (f x) (g (transport B 1 x))) <~>
DPath (fun x : A => B x -> C x) 1 f g
  apply equiv_path_forall.
Defined.

Notation dp_arrow := equiv_dp_arrow.

(* Restricted version allowing us to pull the domain of a forall out *)
Definition equiv_dp_forall_domain `{Funext} {D : Type} {A : Type} {B : D -> A -> Type}
  {t1 t2 : D} {d : t1 = t2} {f : forall x, B t1 x} {g : forall x, B t2 x}
  : (forall x, DPath (fun t => B t x) d (f x) (g x))
   <~> DPath (fun t => forall x, B t x) d f g.H: Funext
D, A: Type
B: D -> A -> Type
t1, t2: D
d: t1 = t2
f: forall x : A, B t1 x
g: forall x : A, B t2 x
(forall x : A,
 DPath (fun t : D => B t x) d (f x) (g x)) <~>
DPath (fun t : D => forall x : A, B t x) d f g
Proof.H: Funext
D, A: Type
B: D -> A -> Type
t1, t2: D
d: t1 = t2
f: forall x : A, B t1 x
g: forall x : A, B t2 x
(forall x : A,
 DPath (fun t : D => B t x) d (f x) (g x)) <~>
DPath (fun t : D => forall x : A, B t x) d f g
  destruct d.H: Funext
D, A: Type
B: D -> A -> Type
t1: D
f, g: forall x : A, B t1 x
(forall x : A,
 DPath (fun t : D => B t x) 1 (f x) (g x)) <~>
DPath (fun t : D => forall x : A, B t x) 1 f g
  apply equiv_path_forall.
Defined.

Notation dp_forall_domain := equiv_dp_forall_domain.

Definition equiv_dp_sigma {A : Type} {B : A -> Type}
  {C : sig B -> Type} {x1 x2 : A} {p : x1 = x2}
  (y1 : { y : B x1 & C (x1; y) }) (y2 : { y : B x2 & C (x2; y) })
  : {n : DPath B p y1.1 y2.1 & DPath C (path_sigma_dp (p; n)) y1.2 y2.2}
    <~> DPath (fun x => { y : B x & C (x; y) }) p y1 y2.A: Type
B: A -> Type
C: {x : _ & B x} -> Type
x1, x2: A
p: x1 = x2
y1: {y : B x1 & C (x1; y)}
y2: {y : B x2 & C (x2; y)}
{n : DPath B p y1.1 y2.1 &
DPath C (path_sigma_dp (p; n)) y1.2 y2.2} <~>
DPath (fun x : A => {y : B x & C (x; y)}) p y1 y2
Proof.A: Type
B: A -> Type
C: {x : _ & B x} -> Type
x1, x2: A
p: x1 = x2
y1: {y : B x1 & C (x1; y)}
y2: {y : B x2 & C (x2; y)}
{n : DPath B p y1.1 y2.1 &
DPath C (path_sigma_dp (p; n)) y1.2 y2.2} <~>
DPath (fun x : A => {y : B x & C (x; y)}) p y1 y2
  destruct p.A: Type
B: A -> Type
C: {x : _ & B x} -> Type
x1: A
y1, y2: {y : B x1 & C (x1; y)}
{n : DPath B 1 y1.1 y2.1 &
DPath C (path_sigma_dp (1%path; n)) y1.2 y2.2} <~>
DPath (fun x : A => {y : B x & C (x; y)}) 1 y1 y2
  refine (path_sigma_dp oE _).A: Type
B: A -> Type
C: {x : _ & B x} -> Type
x1: A
y1, y2: {y : B x1 & C (x1; y)}
{n : DPath B 1 y1.1 y2.1 &
DPath C (path_sigma_dp (1%path; n)) y1.2 y2.2} <~>
{p : y1.1 = y2.1 &
DPath (fun y : B x1 => C (x1; y)) p y1.2 y2.2}
  apply equiv_functor_sigma_id.A: Type
B: A -> Type
C: {x : _ & B x} -> Type
x1: A
y1, y2: {y : B x1 & C (x1; y)}
forall a : DPath B 1 y1.1 y2.1,
DPath C (path_sigma_dp (1%path; a)) y1.2 y2.2 <~>
DPath (fun y : B x1 => C (x1; y)) a y1.2 y2.2
  cbn; intro q.A: Type
B: A -> Type
C: {x : _ & B x} -> Type
x1: A
y1, y2: {y : B x1 & C (x1; y)}
q: transport B 1 y1.1 = y2.1
transport C
  (path_sigma_uncurried B (x1; y1.1) (x1; y2.1)
     (1%path; q)) y1.2 = y2.2 <~>
transport (fun y : B x1 => C (x1; y)) q y1.2 = y2.2
  destruct y1 as [y11 y12], y2 as [y21 y22].A: Type
B: A -> Type
C: {x : _ & B x} -> Type
x1: A
y11: B x1
y12: C (x1; y11)
y21: B x1
y22: C (x1; y21)
q: transport B 1 (y11; y12).1 = (y21; y22).1
transport C
  (path_sigma_uncurried B (x1; (y11; y12).1)
     (x1; (y21; y22).1) (1%path; q)) (y11; y12).2 =
(y21; y22).2 <~>
transport (fun y : B x1 => C (x1; y)) q (y11; y12).2 =
(y21; y22).2
  cbn in *.A: Type
B: A -> Type
C: {x : _ & B x} -> Type
x1: A
y11: B x1
y12: C (x1; y11)
y21: B x1
y22: C (x1; y21)
q: y11 = y21
transport C
  (path_sigma_uncurried B (x1; y11) (x1; y21)
     (1%path; q)) y12 = y22 <~>
transport (fun y : B x1 => C (x1; y)) q y12 = y22
  by destruct q.
Defined.

Notation dp_sigma := equiv_dp_sigma.