dp_apD_compose' {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 o f) p = (dp_compose' f P r)^-1 (apD g q). Proof. by destruct r, p. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.