{ lelt : No -> A & (forall (x y : No), (x <= y) -> forall z, ((lelt y).1 z -> (lelt x).1 z) * ((lelt y).2.1 z -> (lelt x).2.1 z)) * (forall (x y : No), (x < y) -> forall z, ((lelt y).1 z -> (lelt x).2.1 z)) }. Proof. simple refine (No_rec_package A (fun dm ht => forall y, (ht.1 y -> dm.1 y) * (ht.2.1 y -> dm.2.1 y)) (fun dm ht => forall y, (ht.1 y -> dm.2.1 y)) _ _ _ _ _). - intros L R ? xL xR xcut xL_let xR_let x_lt_le. pose (x := {{ xL | xR // xcut }}). exists (fun y => fst (inner xL_let xR_let x_lt_le y).1). exists (fun y => snd (inner xL_let xR_let x_lt_le y).1). abstract ( repeat split; [ intros y; exact (fst (fst (inner xL_let xR_let x_lt_le y).2)) | intros y z x_le_y y_le_z; exact (fst (inner_le xL_let xR_let x_lt_le y z y_le_z) x_le_y) | intros y z x_le_y y_lt_z; exact (inner_lt xL_let xR_let x_lt_le y z y_lt_z x_le_y) | intros y z x_lt_y y_le_z; exact (snd (inner_le xL_let xR_let x_lt_le y z y_le_z) x_lt_y) ]). - abstract ( intros [x_le [x_lt ?]] [x_le' [x_lt' ?]] p q; cbn in p, q; simple refine (path_sigma' _ _ _); [ apply path_arrow; intros y; apply path_hprop, equiv_iff_hprop; [ exact (fst (q y)) | exact (fst (p y)) ] | rewrite transport_sigma'; cbn; simple refine (path_sigma' _ _ _); [ apply path_arrow; intros y; apply path_hprop, equiv_iff_hprop; [ exact (snd (q y)) | exact (snd (p y)) ] | apply path_ishprop ] ] ). - abstract ( intros L R ? xL xR xcut xL_let xR_let x_le_lt L' R' ? yL yR ycut yL_let yR_let y_le_lt; set (x := {{ xL | xR // xcut }}); set (y := {{ yL | yR // ycut }}); cbn; intros xL_lt_y xL_lt_z x_lt_yR le_lt_y; refine (No_ind_hprop _ _); intros L'' R'' ? zL zR zcut zLH zRH; split; [ rewrite !inner_cut_le; intros y_le_z; split; [ intros l; refine (xL_lt_z l {{ zL | zR // zcut }} y_le_z) | intros r; refine (snd (zRH r) (snd y_le_z r)) ] | rewrite !inner_cut_lt; intros y_lt_z; strip_truncations; destruct y_lt_z as [[l y_le_zL]|[r yR_le_z]]; [ apply tr; left; exact (l; fst (zLH l) y_le_zL) | refine (le_lt_y r {{ zL | zR // zcut }} yR_le_z) ]] ). - abstract ( intros L R ? xL xR xcut xL_let xR_let x_le_lt L' R' ? yL yR ycut yL_let yR_let y_le_lt; set (x := {{ xL | xR // xcut }}); set (y := {{ yL | yR // ycut }}); cbn; intros l x_le_yL zH; refine (No_ind_hprop _ _); intros L'' R'' ? zL zR zcut zLH zRH y_le_z; refine (snd (zH {{ zL | zR // zcut }}) _); rewrite inner_cut_le in y_le_z; exact (fst y_le_z l) ). - abstract ( intros L R ? xL xR xcut xL_let xR_let x_le_lt L' R' ? yL yR ycut yL_let yR_let y_le_lt; set (x := {{ xL | xR // xcut }}); set (y := {{ yL | yR // ycut }}); cbn; intros r xR_le_y zH; refine (No_ind_hprop _ _); intros L'' R'' ? zL zR zcut zLH zRH y_le_z; rewrite inner_cut_lt; apply tr; right; exists r; refine (fst (zH {{ zL | zR // zcut }}) y_le_z) ). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.