Proposition prod_prebilattices_are_interlaced {X1 X2 : hSet} {l1 : lattice X1} {l2 : lattice X2} (b : prod_prebilattice X1 X2 l1 l2) : is_interlaced b . Proof. do 3 (try use make_dirprod); intros [x1 x2] [y1 y2] [z1 z2] H; use dirprod_paths; cbn in H; set (H1 := maponpaths dirprod_pr1 H); cbn in H1; set (H2 := maponpaths dirprod_pr2 H); cbn in H2; cbn. - rewrite (iscomm_Lmin _ x1 z1), isassoc_Lmin, <- (isassoc_Lmin _ x1 y1 z1), H1, (iscomm_Lmin _ x1 z1), <- isassoc_Lmin, Lmin_id; reflexivity . - use Lmax_ge_eq_l; use Lmin_ge_case. -- use (istrans_Lge _ x2 y2 (Lmin _ y2 z2)). --- rewrite <- H2; exact (Lmax_ge_r _ x2 y2). --- exact (Lmin_ge_l _ y2 z2). -- exact (Lmin_ge_r _ y2 z2). - use Lmin_ge_eq_l; use Lmax_ge_case. -- use (istrans_Lle _ x1 y1 (Lmax _ y1 z1)). --- rewrite <- H1; exact (Lmin_ge_r _ x1 y1). --- exact (Lmax_ge_l _ y1 z1). -- exact (Lmax_ge_r _ y1 z1). - rewrite (iscomm_Lmax _ x2 z2), (isassoc_Lmax), <- (isassoc_Lmax _ x2 y2 z2), H2, (iscomm_Lmax _ x2 z2), <- isassoc_Lmax, Lmax_id. reflexivity. - rewrite (iscomm_Lmin _ x1 z1), isassoc_Lmin, <- (isassoc_Lmin _ x1 y1 z1), H1, (iscomm_Lmin _ x1 z1), <- isassoc_Lmin, Lmin_id; reflexivity . - use Lmin_ge_eq_l. use Lmax_le_case. -- use (istrans_Lle _ x2 y2 (Lmax _ y2 z2)). --- rewrite <- H2. exact (Lmin_le_r _ x2 y2). --- exact (Lmax_ge_l _ y2 z2). -- exact (Lmax_le_r _ y2 z2). - use Lmin_ge_eq_l; use Lmax_ge_case. -- use (istrans_Lle _ x1 y1 (Lmax _ y1 z1)). --- rewrite <- H1; exact (Lmin_ge_r _ x1 y1). --- exact (Lmax_ge_l _ y1 z1). -- exact (Lmax_ge_r _ y1 z1). - rewrite (iscomm_Lmin _ x2 z2), (isassoc_Lmin), <- (isassoc_Lmin _ x2 y2 z2), H2, (iscomm_Lmin _ x2 z2), <- isassoc_Lmin, Lmin_id. reflexivity. 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.