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