Definition is_distributive_prebilattice {X : hSet} (b : prebilattice X) := isldistr (gullibility b) (consensus b) × isldistr (join b) (meet b) × isldistr (consensus b) (meet b) × isldistr (meet b) (consensus b) × isldistr (consensus b) (join b) × isldistr (join b) (consensus b) × isldistr (gullibility b) (meet b) × isldistr (meet b) (gullibility b) × isldistr (gullibility b) (join b) × isldistr (join b) (gullibility b) .
Require Import UniMath.OrderTheory.Prebilattice.Prebilattice. Require Import UniMath.OrderTheory.Prebilattice.Interlaced. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Distributive.