(n : trunc_index) (X : Type) `{In (nSep n.+1 (Meet L O)) X} : In (nSep n (Meet L O)) (Plus L O X). Proof. apply nsep_iff_trunc_plus. nrefine (mapinO_homotopic _ _ (fun u => (wellpointed_plus L O X u)^)). apply mapinO_tr_istruncmap, istruncmap_plus_functor. - apply istruncmap_mapinO_tr, nsep_iff_trunc_plus; assumption. - apply plusconnmap_to_plus. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.