(n : trunc_index) (O : Modality) `{Lex O} (A : Type) : In (nSep n O) A <-> IsTruncMap n (to O A). Proof. revert A; induction n as [|n IHn]; intros A; split; intros ?. - apply contr_map_isequiv; rapply isequiv_to_O_inO. - apply (inO_equiv_inO (O A) (to O A)^-1). - apply istruncmap_from_ap; intros x y. pose (i := fst (IHn (x = y)) _). apply istruncmap_mapinO_tr, (mapinO_homotopic _ _ (equiv_path_O_to_O O x y)). - intros x y. apply (snd (IHn (x = y))). pose (i := istruncmap_ap n (to O A) x y). apply mapinO_tr_istruncmap in i. apply istruncmap_mapinO_tr, (mapinO_homotopic _ ((equiv_path_O O x y)^-1 o (@ap _ _ (to O A) x y))). { intros p; apply moveR_equiv_V; symmetry; apply equiv_path_O_to_O. } pose mapinO_isequiv. rapply mapinO_compose. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.