Type := GenNo DecSort. Global Instance insort_decsort {L R : Type} {dl : Decidable L} {dr : Decidable R} : InSort DecSort L R | 100 := (dl , dr). Global Instance isequiv_DecNo_raise `{Univalence} : IsEquiv (@No_raise DecSort). Proof. apply isequiv_surj_emb; try exact _. apply BuildIsSurjection; intros x. apply tr. revert x; refine (No_ind_hprop _ _). intros L R s xL xR xcut IHL IHR. pose (uLR := Unit + (L + R)). assert (Decidable uLR) by exact (inl (inl tt)). pose (xLR := sum_ind _ (fun _ => zero) (sum_ind (fun _ => ) (fun l => (IHL l).1) (fun r => (IHR r).1)) : uLR -> ). pose (z := {{ xLR | Empty_rec // rempty_cut }}). pose (z' := {{ unit_name z | Empty_rec // rempty_cut }}). pose (y := {{ Empty_rec | xLR // lempty_cut }}). pose (y' := {{ Empty_rec | unit_name y // lempty_cut }} ). pose (L' := Unit + L). assert (Decidable L') by exact (inl (inl tt)). pose (wL := sum_ind _ (fun _ => y') (fun l => (IHL l).1) : L' -> ). pose (R' := Unit + R). assert (Decidable R') by exact (inl (inl tt)). pose (wR := sum_ind _ (fun _ => z') (fun r => (IHR r).1) : R' -> ). assert (wcut : forall l r, wL l < wR r). { intros [[]|l] [[]|r]; cbn. - transitivity y. { refine (lt_ropt _ _ _ tt). } transitivity z. { apply lt_l with (inl tt); cbn. apply le_lr; intros []. } { refine (lt_lopt _ _ _ tt). } - transitivity y. { refine (lt_ropt _ _ _ tt). } { refine (lt_ropt _ _ _ (inr (inr r))). } - transitivity z. { refine (lt_lopt _ _ _ (inr (inl l))). } { refine (lt_lopt _ _ _ tt). } - apply No_raise_reflects_lt. rewrite (IHL l).2, (IHR r).2. apply xcut. } exists ({{ wL | wR // wcut }}). destruct (No_raise_cut wL wR wcut) as [rwcut p]. rewrite p; clear p. apply path_No; apply le_lr. - intros [[]|l]. + apply (lt_le_trans (y := No_raise y)). * apply No_raise_lt. refine (lt_ropt _ _ _ tt). * unfold y. rewrite (No_raise_cut _ _ _).2. apply le_lr; [ intros [] | intros r ]. rewrite <- (IHR r).2. refine (lt_ropt _ _ _ (inr (inr r))). + rewrite (IHL l).2. refine (lt_lopt _ _ _ l). - intros r. rewrite <- (IHR r).2. refine (lt_ropt _ _ _ (inr r)). - intros l. rewrite <- (IHL l).2. refine (lt_lopt _ _ _ (inr l)). - intros [[]|r]. + apply (le_lt_trans (y := No_raise z)). * unfold z. rewrite (No_raise_cut _ _ _).2. apply le_lr; [ intros l | intros [] ]. rewrite <- (IHL l).2. refine (lt_lopt _ _ _ (inr (inl l))). * apply No_raise_lt. refine (lt_lopt _ _ _ tt). + rewrite (IHR r).2. refine (lt_ropt _ _ _ r). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.