No -> No. Proof. simple refine (No_rec No (fun x y => y <= x) (fun x y => y < x) _ _ _ _ _); intros. - exact {{ fxR | fxL // fun r l => fxcut l r }}. - apply path_No; assumption. - cbn in *. apply le_lr; intros; [ apply dq | apply dp ]. - cbn in *. apply lt_r with l; intros; assumption. - cbn in *. apply lt_l with r; intros; assumption. Defined.
Require Import HoTT.Basics. Require Import HoTT.Spaces.No.Core.