`{Funext} {L R : Type} {s : InSort S L R} (xL : L -> No) (xR : R -> No) {L' R' : Type} {s' : InSort S L' R'} (xL' : L' -> No) (xR' : R' -> No) (eL : L <~> L') (eR : R <~> R') (xLeq : forall l, xL l = xL' (eL l)) (xReq : forall r, xR r = xR' (eR r)) (xcut : forall (l:L) (r:R), (xL l) < (xR r)) (xcut' : forall (l:L') (r:R'), (xL' l) < (xR' r)) : {{ xL | xR // xcut }} = {{ xL' | xR' // xcut' }}. Proof. apply path_No; apply le_lr; [ intros l; rewrite xLeq | intros r; rewrite <- (eisretr eR r), <- xReq | intros l; rewrite <- (eisretr eL l), <- xLeq | intros r; rewrite xReq ]; try apply lt_lopt; try apply lt_ropt. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.