conn_map_O_leq'@{a i1 i2} (O1 : ReflectiveSubuniverse@{i1}) (O2 : ReflectiveSubuniverse@{i2}) `{IsAccRSU@{a i1} O1} `{O_leq@{i1 i2 i2} O1 O2} {A B : Type@{i2}} (f : A -> B) `{IsConnMap O2 A B f} : IsConnMap O1 f. Proof. intros b. apply (isconnected_equiv' O1 (hfiber@{i2 i2} f b)). - srapply equiv_adjointify. 1-2:intros [u p]; exact (u;p). all:intros [u p]; reflexivity. - apply (isconnected_O_leq' O1 O2). apply isconnected_hfiber_conn_map. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.