(** Some examples of lattices. *)
Require Export HoTT lattice_interface.
From HoTT.Classes.implementations Require Export hprop_lattice bool pointwise.