Definition prebilattice_transportf {X1 X2 : hSet} (b1 : prebilattice X1) (b2 : prebilattice X2) (p : X1 = X2) (m : meet (transportf prebilattice p b1) ~ meet b2) (j : join (transportf prebilattice p b1) ~ join b2) (c : consensus (transportf prebilattice p b1) ~ consensus b2) (g : gullibility (transportf prebilattice p b1) ~ gullibility b2) : transportf prebilattice p b1 = b2.
Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.