Lemma islatticewithgtrel_weq {X Y : hSet} (H : weq Y X) {gt : StrongOrder X} (lat : lattice X) : islatticewithgtrel lat gt → islatticewithgtrel (lattice_weq H lat) (StrongOrder_bck H gt). Proof. intros Hgt. split ; split. - intros Hngt. unfold Lle ; simpl. unfold binop_weq_bck. rewrite (pr1 (pr1 Hgt _ _)). apply homotinvweqweq. apply Hngt. - intros Hle. apply (pr2 (pr1 Hgt _ _)). unfold Lle ; simpl. apply pathsinv0, pathsweq1', pathsinv0. apply Hle. - simpl ; intros x y z Hx Hy. unfold binop_weq_bck, fun_hrel_comp. rewrite homotweqinvweq. apply (pr1 (pr2 Hgt)). exact Hx. exact Hy. - unfold Lmax ; simpl ; intros x y z Hx Hy. unfold binop_weq_bck, fun_hrel_comp. rewrite homotweqinvweq. apply (pr2 (pr2 Hgt)). exact Hx. exact Hy. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.