{ f : No -> A & (forall (x y : No) (p : x <= y), dle (f x) (f y)) * (forall (x y : No) (p : x < y), dlt (f x) (f y)) } := ( No_rec ; (No_rec_le , No_rec_lt) ).
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.