(cancel : forall {Y X Z : Type} (f : Y -> X) (g : X -> Z), (IsConnMap O (g o f)) -> (IsConnMap O g) -> IsConnMap O f) : Lex O. Proof. apply lex_from_modal_over_connected_isconst; intros. exists (O {x:A & P x}); split; [ exact _ | intros x; symmetry ]. refine (Build_Equiv _ _ (fun p => to O _ (x ; p)) _). nrefine (isequiv_conn_map_ino O _). 1-2:exact _. revert x; apply conn_map_fiber. nrefine (cancel _ _ _ _ (fun z:{x:A & O {x : A & P x}} => z.2) _ _). 1: clear cancel; exact _. intros z. refine (isconnected_equiv' O A _ _). unfold hfiber. refine (equiv_adjointify (fun x => ((x ; z) ; 1)) (fun y => y.1.1) _ _). - intros [[x y] []]; reflexivity. - intros x; reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.