Lemma is_univalent_prebilattice_disp_category : is_univalent (prebilattice_disp_category) . Proof. use SIP. - use Univalence.is_univalent_HSET. - use isaset_prebilattice. - intros X b1 b2 p1 p2. use prebilattice_eq; intro x; use weqfunextsec; intro y. -- exact (pr1 (p2 x y)). -- exact (pr12 (p2 x y)). -- exact (pr122 (p2 x y)). -- exact (pr222 (p2 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.