Definition truncminus {X : abmonoid} {lat : lattice X} (ex : extruncminus lat) : binop X := pr1 ex.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.