Lemma iscomp_gullibility_rel_same_SW2NE {X : hSet} (b : interlaced_prebilattice X) : iscomprelrelfun2 (eqrel_same_SW2NE b) (eqrel_same_SW2NE b) (gullibility b). Proof. intros x y w z H1 H2. use (isantisymm_Lle (tlattice b) (join _ (gullibility _ x w) (gullibility _ y z)) ((consensus _ (gullibility _ x w) (gullibility _ y z)))). - use Lmax_le_case. -- rewrite iscomm_consensus. use (interlaced_leqt_leqk_leqtconsensus _ (gullibility _ x w) (gullibility _ y z)). exists (gullibility b (join b x y) (join b w z)). split. ---use (double_interlacing_gullibility_t (Lmax_le_l _ x y) (Lmax_le_l _ w z)). --- rewrite H1, H2. use Lmax_le_case. ---- use (istrans_Lle _ _ y _). ----- use Lmin_le_r. ----- use Lmax_le_l. ---- use (istrans_Lle _ _ z _). ----- use Lmin_le_r. ----- use Lmax_le_r. -- use (interlaced_leqt_leqk_leqtconsensus _ (gullibility _ y z) (gullibility _ x w)). exists (gullibility b (join b x y) (join b w z)). split. --- use (double_interlacing_gullibility_t (Lmax_le_r _ _ _) (Lmax_le_r _ _ _)). --- rewrite H1, H2. use Lmax_le_case. ---- use (istrans_Lle _ _ x _). ----- use Lmin_le_l. ----- use Lmax_le_l. ---- use (istrans_Lle _ _ w _). ----- use Lmin_le_l. ----- use Lmax_le_r. - use (top_interlacing_consensus_t (Lmax_le_l _ _ _) (Lmax_le_r _ _ _)). 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.