proposition: Lemma isassocmonob {X Y : setwithbinop} (f : binopmono X Y) (is : isassoc (@op Y)) : isassoc (@op X).
proof: Proof. set (axf := pr2 f). simpl in axf. intros a b c. apply (invmaponpathsincl _ (pr2 (pr1 f))). rewrite (axf (op a b) c). rewrite (axf a b). rewrite (axf a (op b c)). rewrite (axf b c). apply is. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions