dp_apD_compose_inv' {A B : Type} (f : A -> B) (P : B -> Type) {x y : A} {p : x = y} {q : f x = f y} (r : ap f p = q) (g : forall b:B, P b) : apD g q = (dp_compose' f P r) (apD (g o f) p). Proof. by destruct r, p. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.