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. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.