Refactoring frames (#603)

src/order-theory.lagda.md

@@ -45,6 +45,7 @@ open import order-theory.lower-types-preorders public
 open import order-theory.maximal-chains-posets public
 open import order-theory.maximal-chains-preorders public
 open import order-theory.meet-semilattices public
+open import order-theory.meet-suplattices public
 open import order-theory.order-preserving-maps-posets public
 open import order-theory.order-preserving-maps-preorders public
 open import order-theory.posets public

src/order-theory/frames.lagda.md

@@ -13,8 +13,11 @@ open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
 
+open import order-theory.greatest-lower-bounds-posets
 open import order-theory.infinite-distributive-law
+open import order-theory.least-upper-bounds-posets
 open import order-theory.meet-semilattices
+open import order-theory.meet-suplattices
 open import order-theory.posets
 open import order-theory.suplattices
 ```
@@ -29,85 +32,117 @@ distribute over arbitrary joins.
 There are many equivalent ways to formulate this definition. Our choice here is
 simply motivated by a desire to avoid iterated sigma types.
 
+## Definitions
+
+### The predicate on meet-suplattices to be a frame
+
 ```agda
-Frame : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
-Frame l1 l2 =
-  Σ (Meet-Suplattice l1 l2) (distributive-law-meet-suplattice l1 l2)
+module _
+  {l1 l2 : Level} (L : Meet-Suplattice l1 l2)
+  where
+
+  is-frame-Meet-Suplattice-Prop : Prop (l1 ⊔ lsuc l2)
+  is-frame-Meet-Suplattice-Prop = distributive-law-Meet-Suplattice-Prop L
+
+  is-frame-Meet-Suplattice : UU (l1 ⊔ lsuc l2)
+  is-frame-Meet-Suplattice = type-Prop is-frame-Meet-Suplattice-Prop
+
+  is-prop-is-frame-Meet-Suplattice : is-prop is-frame-Meet-Suplattice
+  is-prop-is-frame-Meet-Suplattice =
+    is-prop-type-Prop is-frame-Meet-Suplattice-Prop
 ```
 
-## Now we retrieve all the information from a frame (i.e. break up all of it's components, etc.)
+### Frames
 
 ```agda
+Frame : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Frame l1 l2 = Σ (Meet-Suplattice l1 l2) is-frame-Meet-Suplattice
+
 module _
   {l1 l2 : Level} (A : Frame l1 l2)
   where
 
+  meet-suplattice-Frame : Meet-Suplattice l1 l2
+  meet-suplattice-Frame = pr1 A
+
+  meet-semilattice-Frame : Meet-Semilattice l1
+  meet-semilattice-Frame =
+    meet-semilattice-Meet-Suplattice meet-suplattice-Frame
+
+  suplattice-Frame : Suplattice l1 l1 l2
+  suplattice-Frame = suplattice-Meet-Suplattice meet-suplattice-Frame
+
   poset-Frame : Poset l1 l1
-  poset-Frame = poset-Meet-Suplattice (pr1 A)
+  poset-Frame = poset-Meet-Suplattice meet-suplattice-Frame
+
+  set-Frame : Set l1
+  set-Frame = set-Poset poset-Frame
 
   type-Frame : UU l1
   type-Frame = type-Poset poset-Frame
 
+  is-set-type-Frame : is-set type-Frame
+  is-set-type-Frame = is-set-type-Poset poset-Frame
+
   leq-Frame-Prop : (x y : type-Frame) → Prop l1
   leq-Frame-Prop = leq-Poset-Prop poset-Frame
 
   leq-Frame : (x y : type-Frame) → UU l1
   leq-Frame = leq-Poset poset-Frame
 
-  is-prop-leq-Frame :
-    (x y : type-Frame) → is-prop (leq-Frame x y)
+  is-prop-leq-Frame : (x y : type-Frame) → is-prop (leq-Frame x y)
   is-prop-leq-Frame = is-prop-leq-Poset poset-Frame
-  refl-leq-Frame :
-    (x : type-Frame) → leq-Frame x x
+
+  refl-leq-Frame : (x : type-Frame) → leq-Frame x x
   refl-leq-Frame = refl-leq-Poset poset-Frame
 
   antisymmetric-leq-Frame :
-    (x y : type-Frame) →
-    leq-Frame x y → leq-Frame y x → x ＝ y
-  antisymmetric-leq-Frame =
-    antisymmetric-leq-Poset poset-Frame
+    (x y : type-Frame) → leq-Frame x y → leq-Frame y x → x ＝ y
+  antisymmetric-leq-Frame = antisymmetric-leq-Poset poset-Frame
 
   transitive-leq-Frame :
-    (x y z : type-Frame) →
-    leq-Frame y z → leq-Frame x y →
-    leq-Frame x z
+    (x y z : type-Frame) → leq-Frame y z → leq-Frame x y → leq-Frame x z
   transitive-leq-Frame = transitive-leq-Poset poset-Frame
 
-  is-set-type-Frame : is-set type-Frame
-  is-set-type-Frame = is-set-type-Poset poset-Frame
-
-  set-Frame : Set l1
-  set-Frame = set-Poset poset-Frame
+  meet-Frame : type-Frame → type-Frame → type-Frame
+  meet-Frame = meet-Meet-Semilattice meet-semilattice-Frame
 
-  meet-semilattice-Frame : Meet-Semilattice l1
-  meet-semilattice-Frame = meet-semilattice-Meet-Suplattice (pr1 A)
+  is-greatest-binary-lower-bound-meet-Frame :
+    (x y : type-Frame) →
+    is-greatest-binary-lower-bound-Poset poset-Frame x y (meet-Frame x y)
+  is-greatest-binary-lower-bound-meet-Frame =
+    is-greatest-binary-lower-bound-meet-Meet-Semilattice meet-semilattice-Frame
 
-  is-suplattice-Frame :
-    is-suplattice-Poset l2 poset-Frame
-  is-suplattice-Frame = is-suplattice-Meet-Suplattice (pr1 A)
+  associative-meet-Frame :
+    (x y z : type-Frame) →
+    meet-Frame (meet-Frame x y) z ＝ meet-Frame x (meet-Frame y z)
+  associative-meet-Frame =
+    associative-meet-Meet-Semilattice meet-semilattice-Frame
 
-  suplattice-Frame : Suplattice l1 l1 l2
-  suplattice-Frame = ( poset-Frame , is-suplattice-Frame)
+  commutative-meet-Frame :
+    (x y : type-Frame) → meet-Frame x y ＝ meet-Frame y x
+  commutative-meet-Frame =
+    commutative-meet-Meet-Semilattice meet-semilattice-Frame
 
-  meet-suplattice-Frame :
-    Meet-Suplattice l1 l2
-  meet-suplattice-Frame = pr1 A
+  idempotent-meet-Frame :
+    (x : type-Frame) → meet-Frame x x ＝ x
+  idempotent-meet-Frame =
+    idempotent-meet-Meet-Semilattice meet-semilattice-Frame
 
-  meet-Frame :
-    (x y : type-Frame) →
-    type-Frame
-  meet-Frame = meet-Meet-Semilattice meet-semilattice-Frame
+  is-suplattice-Frame :
+    is-suplattice-Poset l2 poset-Frame
+  is-suplattice-Frame = is-suplattice-Suplattice suplattice-Frame
 
-  sup-Frame :
-    (I : UU l2) → (I → type-Frame) →
-    type-Frame
-  sup-Frame I b = pr1 (is-suplattice-Frame I b)
+  sup-Frame : {I : UU l2} → (I → type-Frame) → type-Frame
+  sup-Frame = sup-Suplattice suplattice-Frame
 
-  distributive-law-Frame :
-    distributive-law-meet-suplattice l1 l2 meet-suplattice-Frame
-  distributive-law-Frame = pr2 A
+  is-least-upper-bound-sup-Frame :
+    {I : UU l2} (x : I → type-Frame) →
+    is-least-upper-bound-family-of-elements-Poset poset-Frame x (sup-Frame x)
+  is-least-upper-bound-sup-Frame =
+    is-least-upper-bound-sup-Suplattice suplattice-Frame
 
-  frame-Frame : Frame l1 l2
-  pr1 frame-Frame = meet-suplattice-Frame
-  pr2 frame-Frame = distributive-law-Frame
+  distributive-meet-sup-Frame :
+    distributive-law-Meet-Suplattice meet-suplattice-Frame
+  distributive-meet-sup-Frame = pr2 A
 ```

src/order-theory/homomorphisms-meet-sup-lattices.lagda.md

@@ -15,6 +15,7 @@ open import foundation.universe-levels
 open import order-theory.homomorphisms-meet-semilattices
 open import order-theory.homomorphisms-sup-lattices
 open import order-theory.infinite-distributive-law
+open import order-theory.meet-suplattices
 open import order-theory.order-preserving-maps-posets
 ```
 

src/order-theory/homomorphisms-sup-lattices.lagda.md

@@ -40,7 +40,7 @@ module _
     is-least-upper-bound-family-of-elements-Poset
       ( poset-Suplattice B)
       ( f ∘ b)
-      ( f (sup-Suplattice A I b))
+      ( f (sup-Suplattice A b))
 
   hom-Suplattice : UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ l4 ⊔ l5)
   hom-Suplattice =