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