contr_partial_Nrec_zero@{} : Contr (partial_Nrec zero). Proof. unfold partial_Nrec. srefine (istrunc_equiv_istrunc {f0 : {f : {m : N & m <= zero} -> X & (f (zero_seg zero) = x0)} & (forall mh : {m : N & m < zero}, f0.1 (succ_seg zero mh) = xs (f0.1 ((equiv_N_segment zero)^-1 (inl mh))))} _). - exact _. - refine (_ oE equiv_inverse (equiv_sigma_assoc _ _)). apply equiv_functor_sigma_id; intros f. cbn; apply equiv_sigma_prod0. - refine (@istrunc_sigma@{nr nr nr} _ _ _ _ _). + srefine (Build_Contr _ _ _). * exists (fun _ => x0); reflexivity. * intros [g H]. srefine (path_sigma _ _ _ _ _); cbn. { apply path_forall; intros m. exact (H^ @ ap g (path_ishprop _ _)). } { rewrite transport_paths_Fl. rewrite ap_apply_l. rewrite ap10_path_forall. rewrite inv_pp, inv_V, concat_p1. transitivity ((ap g 1)^ @ H). - apply whiskerR, ap, ap. apply path_ishprop. - apply concat_1p. } + intros [f H]. apply (Build_Contr _ (fun mh => Empty_rec (N_lt_zero mh.1 mh.2))). intros g. apply path_forall; intros m. destruct (N_lt_zero m.1 m.2). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.