fact: Definition isunitalisob {X Y : setwithbinop} (f : binopiso X Y) (is : isunital (@op Y)) : isunital (@op X) := make_isunital ((invmap f) (pr1 is)) (isunitisob f (pr1 is) (pr2 is)).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions