Definition abgrdiffphi (X : abmonoid) (xa : X × X) : X × (totalsubtype X) := pr1 xa ,, make_carrier (λ x : X, htrue) (pr2 xa) tt.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.