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