{A B C D : Type} (f : A -> B) (g : B -> C) (h : C -> D) (a : O A) : O_functor_compose f (h o g) a @ O_functor_compose g h (O_functor f a) = O_functor_compose (g o f) h a @ ap (O_functor h) (O_functor_compose f g a). Proof. revert a; refine (O_ind2paths _ _ _). intros a; unfold composeD, O_functor_compose; cbn. Open Scope long_path_scope. rewrite !O_indpaths_beta, !ap_pp, !ap_V, !concat_p_pp. refine (whiskerL _ (apD _ (to_O_natural f a)^)^ @ _). rewrite O_indpaths_beta. rewrite transport_paths_FlFr, !concat_p_pp. rewrite !ap_V, inv_V. rewrite !concat_pV_p. apply whiskerL. apply inverse2. apply ap_compose. Close Scope long_path_scope. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.