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