Lemma isdecrel_Lle_weq {X Y : hSet} (H : weq Y X) (lat : lattice X) (is' : isdecrel (Lle lat)) : isdecrel (Lle (lattice_weq H lat)). Proof. intros x y. generalize (is' (H x) (H y)). apply sumofmaps ; intros Hmin. - apply ii1, (pathscomp0 (maponpaths (invmap H) Hmin)), homotinvweqweq. - apply ii2. intros Hinv ; apply Hmin. apply pathsinv0, pathsweq1', pathsinv0, Hinv. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.