{B' A' : Type} (f' g' : B' -> A') (h : B -> B') (k : A -> A') (p : k o f == f' o h) (q : k o g == g' o h) `{O_inverts k} `{O_inverts h} : O (Coeq f g) <~> O (Coeq f' g') := Build_Equiv _ _ _ (O_inverts_functor_coeq h k p q).
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.