Definition prebilattice_iso {X1 : hSet} {X2 : hSet} (b1 : prebilattice X1) (b2 : prebilattice X2) (f : weq X1 X2) (p : respects_prebilattice_structure b1 b2 f) : @z_iso prebilattice_disp_category (X1,,b1) (X2,,b2). Proof. set( f' := (pr1weq f,, p) : (prebilattice_disp_category ⟦ X1,, b1, X2,, b2 ⟧)%cat). set (p_inv := weqinv_respects_prebilattice_structure b1 b2 f p). exists f'. exists (invmap f,, p_inv). use make_dirprod. - use total2_paths_f. -- use weqfunextsec. use homotinvweqweq. -- use weqfunextsec. intro x. use weqfunextsec. intro y. do 3 (try use dirprod_paths); use PartA.Unnamed_thm. - use total2_paths_f. -- use weqfunextsec. use homotweqinvweq. -- use weqfunextsec. intro x. use weqfunextsec. intro y. do 3 (try use dirprod_paths); use PartA.Unnamed_thm. 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.