Zle_HProp@{} : Z -> Z -> HProp@{UN}. Proof. apply (@Z_rec2@{Ularge Ularge} _ (@trunctype_istrunc@{Ularge} _ _) (fun q r => Build_HProp (PairT.Tle q r))). intros. apply path_hprop. simpl. apply (PairT.le_respects _);trivial. Defined.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.