fact: Definition coeq_cmp : Coeq f g -> Coeq (O_functor f) (O_functor g) := functor_coeq (to O B) (to O A) (fun y => (to_O_natural f y)^) (fun y => (to_O_natural g y)^).
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout