Lemma isEq_rel_same_SW2NE {X : hSet} (b : interlaced_prebilattice X) : iseqrel (rel_same_SW2NE b). Proof. do 2 (try split). - intros x y z H1 H2. use (isantisymm_Lle (tlattice b)). -- use Lmax_le_case. --- assert (r1 : tle b x (consensus b (consensus b x y) z) ). { use (istrans_tle _ x (consensus b x y)). - rewrite <- H1. apply (Lmax_le_l (tlattice _)). - rewrite (isassoc_consensus _ x y z), (iscomm_consensus _ x y), <- H2, (iscomm_consensus _ x). use interlacing_consensus_t. use Lmin_absorb . } set (r2 := Lmin_le_r _ _ _ : kle b (consensus b (consensus b x y) z) z ). rewrite iscomm_consensus. use (interlaced_leqt_leqk_leqtconsensus _ _ _ (_,,r1,,r2)). --- set (r1 := Lmax_le_r _ _ _ : tle b z (join b (join b x y) z) ). assert (r2 : kle b (join b (join b x y) z) x). { use (istrans_kle _ (join _ (join b x y) z) (join b x y)). - rewrite (isassoc_join _ x y z), (iscomm_join _ x y), H2, (iscomm_join _ x). use interlacing_join_k. use Lmin_le_l. - rewrite H1. use Lmin_le_l. } use (interlaced_leqt_leqk_leqtconsensus _ _ _ (_,,r1,,r2)). -- use (top_interlacing_consensus_t (Lmax_le_l _ x z) (Lmax_le_r _ x z)). - intro. unfold rel_same_SW2NE, consensus. rewrite Lmin_id. unfold join. rewrite Lmax_id. reflexivity. - intros ? ? H. unfold rel_same_SW2NE. rewrite iscomm_join, iscomm_consensus. exact H. 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.