Lemma Lle_correct_weq {X Y : hSet} (H : weq Y X) (lat : lattice X) : fun_hrel_comp H (Lle lat) = Lle (lattice_weq H lat). Proof. apply funextfun ; intros x. apply funextfun ; intros y. apply hPropUnivalence ; intros Hle. - apply pathsinv0, pathsweq1, pathsinv0. apply Hle. - apply pathsinv0, pathsweq1', pathsinv0. apply Hle. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.