fact: Definition O_functor_square {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) ).
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout