Definition hProp_lattice : lattice (hProp,,isasethProp). Proof. use make_lattice. - intros P Q; exact (P ∧ Q). - simpl; intros P Q; exact (P ∨ Q). - repeat split. + intros P Q R; apply isassoc_hconj. + intros P Q; apply iscomm_hconj. + intros P Q R; apply isassoc_hdisj. + intros P Q; apply iscomm_hdisj. + intros P Q; apply hconj_absorb_hdisj. + intros P Q; apply hdisj_absorb_hconj. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.