proposition: Lemma isldistrmonob {X Y : setwith2binop} (f : twobinopmono X Y) (is : isldistr (@op1 Y) (@op2 Y)) : isldistr (@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 c (op1 a b))) ((pr1 f) (op1 (op2 c a) (op2 c b)))). rewrite (ax2f c (op1 a b)). rewrite (ax1f a b). rewrite (ax1f (op2 c a) (op2 c b)). rewrite (ax2f c a). rewrite (ax2f c b). apply is. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions