Lemma interlaced_carrier_to_prod_carrier {X : hSet} (b : interlaced_prebilattice X) : weq X (prod_prebilattice_carrier (setquotinset (rel_same_SW2NE b)) (setquotinset (rel_same_SE2NW b))) . Proof. exists (λ x, setquotpr (eqrel_same_SW2NE b) x,, setquotpr (eqrel_same_SE2NW b) x). intro y; destruct y as [yL yR]. set (TL := λ yL, λ yR : setquotinset (rel_same_SE2NW b), hfiber (λ x : X, setquotpr (eqrel_same_SW2NE b) x,, setquotpr (eqrel_same_SE2NW b) x) (yL,, yR)). use (setquotunivprop (eqrel_same_SW2NE b) (λ yL, make_hProp (iscontr (TL yL yR)) (isapropiscontr (TL yL yR)))). intro y1. set (TR := λ yR, TL (setquotpr (eqrel_same_SW2NE b) y1) yR). use (setquotunivprop (eqrel_same_SE2NW b) (λ yR, make_hProp (iscontr (TR yR)) (isapropiscontr (TR yR)))). intro y2. set (c := consensus b (meet b y1 (gullibility b y1 y2)) (join b y2 (gullibility b y1 y2))). assert (HL : setquotpr (eqrel_same_SW2NE b) c = setquotpr (eqrel_same_SW2NE b) y1). { use weqpathsinsetquot. use (eqreltrans _ _ (meet b (meet b y1 (gullibility b y1 y2)) (join b y2 (gullibility b y1 y2))) _ ). { use eqrelsymm. use rel_same_SW2NE_meet_consensus. } use (eqreltrans _ _ (meet b (meet b y1 (join b y1 y2)) (join b y2 (join b y1 y2))) _ ). { use iscomp_meet_rel_same_SW2NE. - use iscomp_meet_rel_same_SW2NE. -- use eqrelrefl. -- use eqrelsymm. use rel_same_SW2NE_join_gullibility. - use iscomp_join_rel_same_SW2NE. -- use eqrelrefl. -- use eqrelsymm. use rel_same_SW2NE_join_gullibility. } rewrite meet_join_absorb, iscomm_join, isassoc_join, join_id, meet_join_absorb. use eqrelrefl. } assert (HR : setquotpr (eqrel_same_SE2NW b) c = setquotpr (eqrel_same_SE2NW b) y2). { use weqpathsinsetquot. use (eqreltrans _ _ (join b (meet b y1 (gullibility b y1 y2)) (join b y2 (gullibility b y1 y2))) _ ). { use eqrelsymm. use rel_same_SE2NW_join_consensus. } use (eqreltrans _ _ (join b (meet b y1 (meet b y1 y2)) (join b y2 (meet b y1 y2))) _ ). { use iscomp_join_rel_same_SE2NW. - use iscomp_meet_rel_same_SE2NW. -- use eqrelrefl. -- use eqrelsymm. use rel_same_SE2NW_meet_gullibility. - use iscomp_join_rel_same_SE2NW. -- use eqrelrefl. -- use eqrelsymm. use rel_same_SE2NW_meet_gullibility. } rewrite (iscomm_meet _ y1 (meet _ _ _)), (iscomm_meet _ y1 y2), isassoc_meet, meet_id, join_meet_absorb, iscomm_join, join_meet_absorb. use eqrelrefl. } exists (c,,pathsdirprod HL HR). intro t. use total2_paths_f. - use (! SE2NW_and_SW2NE_is_id _ _ _ (invmap (weqpathsinsetquot _ _ _) (HL @ ! (maponpaths pr1 (pr2 t)))) (invmap (weqpathsinsetquot _ _ _) (HR @ ! (maponpaths dirprod_pr2 (pr2 t)))) ). - use (proofirrelevance_hProp ( @eqset (make_hSet _ (isaset_dirprod (isasetsetquot (eqrel_same_SW2NE b)) (isasetsetquot (eqrel_same_SE2NW b)))) (setquotpr (eqrel_same_SW2NE b) c,, setquotpr (eqrel_same_SE2NW b) c) (setquotpr (eqrel_same_SW2NE b) y1,, setquotpr (eqrel_same_SE2NW b) y2) )). 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.