{A B C X : Type} (pi1 : X -> A) (pi2 : X -> B) (f : A -> C) (g : B -> C) (comm : (f o pi1) == (g o pi2)) : ( (O_functor f) o (O_functor pi1) ) == ( (O_functor g) o (O_functor pi2) ). Proof. intros x. transitivity (O_functor (f o pi1) x). - symmetry; rapply O_functor_compose. - transitivity (O_functor (g o pi2) x). * apply O_functor_homotopy, comm. * rapply O_functor_compose. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.