{ f : forall x, A x & (forall (x y : GenNo) (p : x <= y), dle x y p (f x) (f y)) * (forall (x y : GenNo) (p : x < y), dlt x y p (f x) (f y)) } := ( No_ind ; (No_ind_le , No_ind_lt) ).
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.