(x : No) : A. Proof. revert x; simple refine (No_ind (fun _ => A) (fun _ _ _ a b => dle a b) (fun _ _ _ a b => dlt a b) _ _ _ _ _); intros. - exact (dcut L R _ xL xR xcut fxL fxR fxcut). - refine (transport_const _ _ @ _). apply dpath; assumption. - cbn. apply dle_lr; assumption. - cbn. apply dlt_l with l; assumption. - cbn. apply dlt_r with r; assumption. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.