proposition: Lemma isrdistrmonob {X Y : setwith2binop} (f : twobinopmono X Y) (is : isrdistr (@op1 Y) (@op2 Y)) : isrdistr (@op1 X) (@op2 X).
proof: Proof. set (ax1f := pr1 (pr2 f)). set (ax2f := pr2 (pr2 f)). intros a b c. apply (invmaponpathsincl _ (pr2 (pr1 f))). change (paths ((pr1 f) (op2 (op1 a b) c)) ((pr1 f) (op1 (op2 a c) (op2 b c)))). rewrite (ax2f (op1 a b) c). rewrite (ax1f a b). rewrite (ax1f (op2 a c) (op2 b c)). rewrite (ax2f a c). rewrite (ax2f b c). apply is. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions