proposition: Lemma twobinopiso_paths {X Y : setwith2binop} (f g : twobinopiso X Y) (e : pr1 f = pr1 g) : f = g.
proof: Proof. use total2_paths_f. - exact e. - use proofirrelevance. use isapropistwobinopfun. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions