proposition: Lemma islatticeop_weq {X Y : hSet} (H : weq Y X) {min max : binop X} (lat : islatticeop min max) : islatticeop (binop_weq_bck H min) (binop_weq_bck H max).
proof: Proof. intros. split ; [ | split] ; split. - apply (isassoc_weq_bck H), (isassoc_Lmin (_,,_,,lat)). - apply (iscomm_weq_bck H), (iscomm_Lmin (_,,_,,lat)). - apply (isassoc_weq_bck H), (isassoc_Lmax (_,,_,,lat)). - apply (iscomm_weq_bck H), (iscomm_Lmax (_,,_,,lat)). - apply (isabsorb_weq_bck H), (Lmin_absorb (_,,_,,lat)). - apply (isabsorb_weq_bck H), (Lmax_absorb (_,,_,,lat)). Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups