proposition: 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: 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.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups