{O1 O2 : ReflectiveSubuniverse} (leq : O1 << O2) {X Y : Type} (f : X -> Y) `{IsConnMap O1 _ _ f} : IsConnMap O1 (O_functor O2 f). Proof. rapply (cancelR_conn_map _ (to O2 _)). nrapply conn_map_homotopic. 1: symmetry; apply to_O_natural. rapply conn_map_compose. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.