{A} (B : A -> Type) (f : forall x:A, B x) {x y : A} {p1 p2 p3 : x = y} (r1 : p1 = p2) (r2 : p2 = p3) : apD02 f (r1 @ r2) = apD02 f r1 @ whiskerL (transport2 B r1 (f x)) (apD02 f r2) @ concat_p_pp _ _ _ @ (whiskerR (transport2_p2p B r1 r2 (f x))^ (apD f p3)). Proof. destruct r1, r2. destruct p1. reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.