Definition op2 {X : apsetwith2binop} : binop X := op2 (X := apsetwith2binop_setwith2binop X).
Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions.