(O O' : ReflectiveSubuniverse) `{O' <= Sep O} {B A B' A'} {f g : B -> A} {f' g' : B' -> A'} (h : B -> B') (k : A -> A') (p : k o f == f' o h) (q : k o g == g' o h) `{IsConnMap O' _ _ k} `{IsConnMap O _ _ h} : IsConnMap O' (functor_coeq h k p q). Proof. apply conn_map_from_extension_elim; intros. apply extension_functor_coeq. - rapply ooextendable_conn_map_inO. - pose (inO_leq O' (Sep O)); intros; rapply (ooextendable_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.