fact: Definition dp_apD_compose {A B : Type} (f : A -> B) (P : B -> Type) {x y : A} (p : x = y) (g : forall b:B, P b) : apD (g o f) p = (dp_compose f P p)^-1 (apD g (ap f p)) := dp_apD_compose' f P (idpath (ap f p)) g.
imports: Basics Types.Paths Types.Sigma Types.Forall