path_No_easy' `{Funext} {L R : Type} {s : InSort S L R} (xL xL' : L -> No) (xR xR' : R -> No) (xLeq : forall l, xL l = xL' l) (xReq : forall r, xR r = xR' r) (xcut : forall (l:L) (r:R), (xL l) < (xR r)) : {{ xL | xR // xcut }} = {{ xL' | xR' // (fun l r => transport (fun xy => fst xy < snd xy) (path_prod' (xLeq l) (xReq r)) (xcut l r)) }} := path_No_easy xL xR xL' xR' 1 1 xLeq xReq xcut _. End OptionSort. Ltac repeat_No_ind_hprop := try match goal with | [ x : GenNo ?S |- _ ] => revert x; repeat_No_ind_hprop; refine (No_ind_hprop _ _); intros ? ? ? ? ? ? ? ? end. Section NoCodes. Context `{Univalence}. Universe i. Context {S : OptionSort@{i}}. Let No := GenNo S. Let A := {le'_x : No -> HProp & {lt'_x : No -> HProp & (forall y : No, lt'_x y -> le'_x y) * (forall y z : No, le'_x y -> y <= z -> le'_x z) * (forall y z : No, le'_x y -> y < z -> lt'_x z) * (forall y z : No, lt'_x y -> y <= z -> lt'_x z)} }. Section Inner. Context {L R : Type@{i} } {s : InSort S L R} (xL : L -> No) (xR : R -> No) (xcut : forall (l : L) (r : R), xL l < xR r) (xL_let : L -> A) (xR_let : R -> A) (x_lt_le : forall (l : L) (r : R) (y : No), (xR_let r).1 y -> ((xL_let l).2).1 y). Let A' (y : No) : Type := { lelt'_x_y : HProp * HProp & (snd lelt'_x_y -> fst lelt'_x_y) * (forall l : L, fst lelt'_x_y -> ((xL_let l).2).1 y) * (forall r : R, (xR_let r).1 y -> snd lelt'_x_y) }. Let A'le (y z : No) (p : y <= z) (tr : A' y) (sq : A' z) : Type := (fst tr.1 -> fst sq.1) * (snd tr.1 -> snd sq.1). Let A'lt (y z : No) (p : y < z) (tr : A' y) (sq : A' z) : Type := (fst tr.1 -> snd sq.1). Local inner_package : { inner : forall (y : No), A' y & (forall y z p, A'le y z p (inner y) (inner z)) * (forall y z p, A'lt y z p (inner y) (inner z)) }. Proof. simple refine (No_ind_package A' A'le A'lt _ _ _ _ _ ); unfold A', A'le, A'lt; try exact _. - intros L' R' ? yL yR ycut x_let_yL x_let_yR y_lt_le. set (y := {{ yL | yR // ycut }}). exists (Build_HProp ((forall l, (xL_let l).2.1 y) * (forall r', snd (x_let_yR r').1)) , (hor {l':L' & fst (x_let_yL l').1} {r:R & (xR_let r).1 y})). abstract ( refine ((_,_),_); [ intros h; strip_truncations; destruct h as [[l' h]|[r h]]; split; intros; [ refine (snd (fst (xL_let l).2.2) (yL l') y _ _); [ refine (fst (fst (fst (xL_let l).2.2)) (yL l') _); exact (snd (fst (x_let_yL l').2) l h) | by (apply lt_lopt; exact _) ] | exact (y_lt_le l' r' h) | exact (x_lt_le l r y h) | refine (snd (x_let_yR r').2 r _); refine (fst (fst (fst (xR_let r).2.2)) _ _); refine (snd (fst (xR_let r).2.2) y (yR r') h _); apply lt_ropt; exact _ ] | intros l [h k]; apply h | intros r h; apply tr, inr; exact (r;h) ] ). - abstract ( intros y z [[x_le_y x_lt_y] ?] [[x_le_z x_lt_z] ?] p q; cbn; intros [p1 p2] [q1 q2]; rewrite transport_sigma'; refine (path_sigma' _ (path_prod' (path_hprop (equiv_iff_hprop p1 q1)) (path_hprop (equiv_iff_hprop p2 q2))) _); apply path_ishprop ). - abstract ( cbn; intros L' R' ? yL yR ycut x_let_yL x_let_yR y_lt_le; set (y := {{ yL | yR // ycut }}); intros L'' R'' ? zL zR zcut x_let_zL x_let_zR z_lt_le; set (z := {{ zL | zR // zcut }}); intros yL_lt_z h1 y_lt_zR h2; assert (y_le_z := le_lr yL yR ycut zL zR zcut yL_lt_z y_lt_zR); split; [ intros [h3 h4]; split | intros h3; strip_truncations; destruct h3 as [[l' h3]|[r h3]] ] ; [ intros l; refine (snd (xL_let l).2.2 y z (h3 l) y_le_z) | intros r''; refine (h2 r'' (h3 , h4)) | refine (h1 l' h3) | apply tr, inr; exists r; refine (snd (fst (fst (xR_let r).2.2)) y z h3 y_le_z) ] ). - abstract ( cbn; intros L' R' ? yL yR ycut x_let_yL x_let_yR y_lt_le; set (y := {{ yL | yR // ycut }}); intros L'' R'' ? zL zR zcut x_let_zL x_let_zR z_lt_le; set (z := {{ zL | zR // zcut }}); intros l'' y_le_zL [h1 h2] x_le_y; apply tr, inl; exact (l''; h1 x_le_y) ). - abstract ( cbn; intros L' R' ? yL yR ycut x_let_yL x_let_yR y_lt_le; set (y := {{ yL | yR // ycut }}); intros L'' R'' ? zL zR zcut x_let_zL x_let_zR z_lt_le; set (z := {{ zL | zR // zcut }}); intros r' yR_le_z [h1 h2] x_le_y; apply h2; exact (snd x_le_y r') ). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.