(A : Type) (P : A -> Type) (f : forall a, P a) {a0 a1 a2 : A} (p : a0 = a1) (q : a1 = a2) : apD f (p @ q) = (apD f p) @Dp (apD f q). Proof. by destruct p, q. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.