{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. Proof. apply equiv_concat_l, transport_paths_Fr. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.