Definition respects_prebilattice_structure {X1 : hSet} {X2 : hSet} (b1 : prebilattice X1) (b2 : prebilattice X2) (f : X1 -> X2) : UU := ∀ x y, make_hProp _ ( isapropdirprod _ _ (setproperty _ (meet b2 (f x) (f y)) (f (meet b1 x y))) (isapropdirprod _ _ (setproperty _ (join b2 (f x) (f y)) (f (join b1 x y))) (isapropdirprod _ _ (setproperty _ (consensus b2 (f x) (f y)) (f (consensus b1 x y)) ) (setproperty _ (gullibility b2 (f x) (f y)) (f (gullibility b1 x y))))) ).
Require Import UniMath.OrderTheory.Prebilattice.Prebilattice. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.