Definition prebilattice_eq {X : hSet} (b1 : prebilattice X) (b2 : prebilattice X) (m : meet b1 ~ meet b2) (j : join b1 ~ join b2) (c : consensus b1 ~ consensus b2) (g : gullibility b1 ~ gullibility b2): b1 = b2. Proof. use (@prebilattice_transportf X X b1 b2 (idpath X)); now rewrite idpath_transportf. Defined.
Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.