(x y : GenNo S) : (No_raise x < No_raise y) -> (x < y) := snd (No_raise_reflects_lelt x y). Global Instance isemb_No_raise : IsEmbedding No_raise. Proof. apply isembedding_isinj_hset. intros x y e; apply path_No. - refine (No_raise_reflects_le x y _). rewrite e; apply reflexive_le. - refine (No_raise_reflects_le y x _). rewrite e; apply reflexive_le. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.