{A B : Type} (f g : A -> B) (pi : f == g) : O_functor_homotopy g f (fun x => (pi x)^) == fun x => (O_functor_homotopy f g pi x)^. Proof. refine (O_ind2paths _ _ _); intros x. unfold composeD, O_functor_homotopy. rewrite !O_indpaths_beta, !ap_V, !inv_pp, inv_V, !concat_p_pp. reflexivity. 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.