{A B : Type} {f g : A -> B} (p q : f == g) (r : p == q) : O_functor_homotopy f g p == O_functor_homotopy f g q. Proof. refine (O_ind2paths _ _ _); intros x. unfold O_functor_homotopy, composeD. do 2 rewrite O_indpaths_beta. apply whiskerL, whiskerR, ap, r. 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.