fact: Definition invtwobinopiso {X Y : setwith2binop} (f : twobinopiso X Y) : twobinopiso Y X := make_twobinopiso (invweq (pr1 f)) (istwobinopfuninvmap f).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions