Lemma iscomp_meet_rel_same_SW2NE {X : hSet} (b : interlaced_prebilattice X) : iscomprelrelfun2 (eqrel_same_SW2NE b) (eqrel_same_SW2NE b) (meet b). Proof. intros x y z w ? ?. use (eqreltrans (eqrel_same_SW2NE b) _ (consensus b x z) _ (rel_same_SW2NE_meet_consensus _ _ _)). use (eqreltrans (eqrel_same_SW2NE b) _ (consensus b y w) _ (iscomp_consensus_rel_same_SW2NE _ _ _ _ _ _ _)). - assumption. - assumption. - use eqrelsymm. use rel_same_SW2NE_meet_consensus. 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.