(n : trunc_index) (X : Type) : In (nSep n (Meet L O)) X <-> MapIn (Tr n) (to_plus L O X). Proof. revert X; induction n as [|n IHn]; intros X; split; intros H. - apply contr_map_isequiv. rapply isequiv_plus_inmeet. - apply inmeet_isequiv_plus. rapply isequiv_contr_map. - apply istruncmap_from_ap; intros x y. apply istruncmap_mapinO_tr. pose (i := fst (IHn _) (H x y)). apply (mapinO_homotopic _ _ (plus_path_to_plus x y)). - intros x y. apply (snd (IHn (x = y))). pose (i := istruncmap_ap n (to_plus L O X) x y). apply mapinO_tr_istruncmap in i. apply (mapinO_homotopic _ ((plus_path x y)^-1 o (@ap _ _ (to_plus L O X) x y))). { intros p; apply moveR_equiv_V; symmetry; apply plus_path_to_plus. } rapply mapinO_compose. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.