Definition hProp_bounded_lattice : bounded_lattice (hProp,,isasethProp). Proof. use make_bounded_lattice. - exact hProp_lattice. - exact hfalse. - exact htrue. - split. + intros P; apply hfalse_hdisj. + intros P; apply htrue_hconj. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.OrderTheory.Lattice.Lattice.