proposition: Lemma isunitisob {X Y : setwithbinop} (f : binopiso X Y) (uny : Y) (is : isunit (@op Y) uny) : isunit (@op X) ((invmap f) uny).
proof: Proof. set (int := isunitisof (invbinopiso f)). simpl. simpl in int. apply int. apply is. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions