{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. Proof. destruct q; exact concat. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.