Lemma rel_same_SE2NW_meet_gullibility {X : hSet} (b : interlaced_prebilattice X) (x y : X) : rel_same_SE2NW b (meet b x y) (gullibility b x y). Proof. use (isantisymm_Lle (tlattice b)). - use (bottom_interlacing_consensus_t (Lmin_le_l _ _ _) (Lmin_le_r _ _ _)). - use Lmin_le_case. -- rewrite iscomm_consensus. use interlaced_leqk_geqt_geqtconsensus. exists (gullibility b x y). split. --- exact (top_interlacing_meet_k (Lmax_le_l _ _ _) (Lmax_le_r _ _ _)). --- use isrefl_Lle. -- use interlaced_geqt_leqk_geqtconsensus . exists (meet b x y). split. --- exact (bottom_interlacing_gullibility_t (Lmin_le_l _ _ _) (Lmin_le_r _ _ _)). --- use isrefl_Lle. 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.