Definition iso_interlaced_product {X : hSet} (b : interlaced_prebilattice X) : @z_iso (precategory_data_from_precategory prebilattice_disp_category) (X,, (pr1 b)) (prod_prebilattice_carrier (pr1 (interlaced_prebilattice_to_prod b)) (pr12 (interlaced_prebilattice_to_prod b)),, (pr1 (make_interlaced_prebilattice (prod_prebilattices_are_interlaced (pr222 (pr2 (interlaced_prebilattice_to_prod b))))))). Proof. use (prebilattice_iso b (make_interlaced_prebilattice (prod_prebilattices_are_interlaced (pr2 (pr222 (interlaced_prebilattice_to_prod b))))) (interlaced_carrier_to_prod_carrier b)). intros x y. do 4 (try use make_dirprod); use dirprod_paths; use pathsinv0; try (use (iscompsetquotpr (eqrel_same_SW2NE _))); try (use (iscompsetquotpr (eqrel_same_SE2NW _))). - use (rel_same_SW2NE_meet_consensus). - use (rel_same_SE2NW_meet_gullibility). - use (rel_same_SW2NE_join_gullibility). - use (rel_same_SE2NW_join_consensus). - use (pr21 (isEq_rel_same_SW2NE _)). - use (pr21 (isEq_rel_same_SE2NW _)). - use (pr21 (isEq_rel_same_SW2NE _)). - use (pr21 (isEq_rel_same_SE2NW _)). Defined.
Require Import UniMath.OrderTheory.Prebilattice.Prebilattice. Require Import UniMath.OrderTheory.Prebilattice.Interlaced. Require Import UniMath.OrderTheory.Prebilattice.PrebilatticeDisplayedCat. Require Import UniMath.MoreFoundations.Equivalences. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.CategoryTheory.Core.Prelude.