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 [DPath]s to collapse to paths under [cbn] *)
Arguments DPath _ / _ _ _ : simpl nomatch.

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 [DPath]s, 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. 

(** Horizontal composition and whiskering of dependent paths *)
Definition dp_concat2 {A} {P : A -> Type} {a0 a1 a2}
  {p : a0 = a1} {q : a1 = a2} {b0 : P a0} {b1 : P a1} {b2 : P a2}
  {r r' : DPath P p b0 b1} {s s' : DPath P q b1 b2}
  (h : r = r') (k : s = s')
  : r @Dp s = r' @Dp s'.A: Type
P: A -> Type
a0, a1, a2: A
p: a0 = a1
q: a1 = a2
b0: P a0
b1: P a1
b2: P a2
r, r': DPath P p b0 b1
s, s': DPath P q b1 b2
h: r = r'
k: s = s'
r @Dp s = r' @Dp s'
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
r, r': DPath P p b0 b1
s, s': DPath P q b1 b2
h: r = r'
k: s = s'
r @Dp s = r' @Dp s'
  by destruct h, k.
Defined.

Definition dp_whiskerL {A: Type} {P : A -> Type} {a0 a1 a2 : A}
  {p : a0 = a1} {q : a1 = a2} {b0 : P a0} {b1 : P a1} {b2 : P a2}
  (r : DPath P p b0 b1) {s s' : DPath P q b1 b2} (h : s = s')
  : r @Dp s = r @Dp s'
  := dp_concat2 1 h.

Definition dp_whiskerR {A: Type} {P : A -> Type} {a0 a1 a2 : A}
  {p : a0 = a1} {q : a1 = a2} {b0 : P a0} {b1 : P a1} {b2 : P a2}
  {r r' : DPath P p b0 b1} (s : DPath P q b1 b2) (h : r = r')
  : r @Dp s = r' @Dp s
  := dp_concat2 h 1.

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.

Definition dp_apD_compose_inv' {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 q = (dp_compose' f P r) (apD (g o f) p).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 q = dp_compose' f P r (apD (g o f) p)
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 q = dp_compose' f P r (apD (g o f) p)
  by destruct r, p.
Defined.

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

(** Type constructors *)

(** Many of these lemmas exist already for transports but we prove them for
   [DPath]s 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 separate, 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.