(O O' : ReflectiveSubuniverse) `{O' <= Sep O} {B A : Type} (f g : B -> A) {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 O' k} `{IsConnMap O _ _ h} : O_inverts O' (functor_coeq h k p q). Proof. apply O_inverts_from_extendable. intros Z Z_inO. apply extendable_functor_coeq. - nrapply (ooextendable_O_inverts O'); assumption. - pose (inO_leq O' (Sep O)). intros u v; rapply (extendable_conn_map_inO O). 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.