(H : forall A B (f : A -> B), (IsConnected O A) -> (IsConnected O B) -> IsConnMap O f) : Lex O. Proof. apply lex_from_cancelL_conn_map. intros Y X Z f g gfc gc x. pose (h := @functor_hfiber Y Z X Z (g o f) g f idmap (fun a => 1%path)). assert (cc := H _ _ (h (g x)) (gfc (g x)) (gc (g x))). refine (isconnected_equiv' O _ _ (cc (x;1))). unfold hfiber. subst h; unfold functor_hfiber, functor_sigma; cbn. refine (_ oE (equiv_sigma_assoc _ _)^-1). apply equiv_functor_sigma_id; intros y; cbn. refine (_ oE (equiv_functor_sigma_id _)). 2:intros; symmetry; apply equiv_path_sigma. cbn. refine (_ oE equiv_sigma_symm _). apply equiv_sigma_contr; intros p. destruct p; cbn. refine (contr_equiv' { p : g (f y) = g (f y) & p = 1%path } _). apply equiv_functor_sigma_id; intros p; cbn. apply equiv_concat_l. exact (concat_1p _ @ ap_idmap _). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.