Definition ispartrdistr {X : abmonoid} (Y : @submonoid X) (opp1 opp2 : binop X) := ∏ (x y : X) (k : Y), opp2 (opp1 x y) (pr1 k) = opp1 (opp2 x (pr1 k)) (opp2 y (pr1 k)).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.