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