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