Definition weqabgrdiffint (X : abmonoid) : weq (X × X) (X × totalsubtype X) := weqdirprodf (idweq X) (invweq (weqtotalsubtype X)).
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.