fact: Definition apD_compose {A A' : Type} {B : A' -> Type} (g : A -> A') (f : forall a, B a) {x y : A} (p : x = y) : apD (f o g) p = (transport_compose _ _ _ _) @ apD f (ap g p).
imports: Basics.Overture Basics.Tactics