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