Definition prebilattice_disp_category : category. Proof. use (@total_category hset_category). use disp_cat_from_SIP_data. - intro X. exact (prebilattice X). - intros X1 X2 b1 b2 f. use (respects_prebilattice_structure b1 b2 f). - intros X1 X2 b1 b2 f p1 p2. use impred_prop. - now intros X1 b1 x y. - intros X1 X2 X3 b1 b2 b3 f g p1 p2 x y. cbn. do 3 (try use make_dirprod). -- now rewrite (pr1 (p2 (f x) (f y))), (pr1 (p1 x y)). -- now rewrite (pr12 (p2 (f x) (f y))), (pr12 (p1 x y)). -- now rewrite (pr122 (p2 (f x) (f y))), (pr122 (p1 x y)). -- now rewrite (pr222 (p2 (f x) (f y))), (pr222 (p1 x y)). Defined.
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.