Cleaning up order theory some more (#599)

src/elementary-number-theory/maximum-natural-numbers.lagda.md

@@ -84,9 +84,14 @@ leq-right-leq-max-ℕ (succ-ℕ k) (succ-ℕ m) (succ-ℕ n) H =
 is-least-upper-bound-max-ℕ :
   (m n : ℕ) → is-least-binary-upper-bound-Poset ℕ-Poset m n (max-ℕ m n)
 is-least-upper-bound-max-ℕ m n =
-  ( leq-left-leq-max-ℕ (max-ℕ m n) m n (refl-leq-ℕ (max-ℕ m n)),
-    leq-right-leq-max-ℕ (max-ℕ m n) m n (refl-leq-ℕ (max-ℕ m n))),
-  λ x (m≤x , n≤x) → leq-max-ℕ x m n m≤x n≤x
+  prove-is-least-binary-upper-bound-Poset
+    ( ℕ-Poset)
+    { m}
+    { n}
+    { max-ℕ m n}
+    ( leq-left-leq-max-ℕ (max-ℕ m n) m n (refl-leq-ℕ (max-ℕ m n)),
+      leq-right-leq-max-ℕ (max-ℕ m n) m n (refl-leq-ℕ (max-ℕ m n)))
+    ( λ x (H , K) → leq-max-ℕ x m n H K)
 ```
 
 ### Associativity of `max-ℕ`

src/elementary-number-theory/maximum-standard-finite-types.lagda.md

@@ -79,10 +79,18 @@ leq-right-leq-max-Fin (succ-ℕ k) (inl x) (inl y) (inr z) p = p
 is-least-upper-bound-max-Fin :
   (k : ℕ) (m n : Fin k) →
   is-least-binary-upper-bound-Poset (Fin-Poset k) m n (max-Fin k m n)
-pr1 (pr1 (is-least-upper-bound-max-Fin k m n)) =
-  leq-left-leq-max-Fin k (max-Fin k m n) m n (refl-leq-Fin k (max-Fin k m n))
-pr2 (pr1 (is-least-upper-bound-max-Fin k m n)) =
-  leq-right-leq-max-Fin k (max-Fin k m n) m n (refl-leq-Fin k (max-Fin k m n))
-pr2 (is-least-upper-bound-max-Fin k m n) x (pair H K) =
-  leq-max-Fin k x m n H K
+is-least-upper-bound-max-Fin k m n =
+  prove-is-least-binary-upper-bound-Poset
+    ( Fin-Poset k)
+    ( ( leq-left-leq-max-Fin k
+        ( max-Fin k m n)
+        ( m)
+        ( n)
+        ( refl-leq-Fin k (max-Fin k m n))) ,
+      ( leq-right-leq-max-Fin k
+        ( max-Fin k m n)
+        ( m)
+        ( n)
+        ( refl-leq-Fin k (max-Fin k m n))))
+    ( λ x (H , K) → leq-max-Fin k x m n H K)
 ```

src/elementary-number-theory/minimum-natural-numbers.lagda.md

@@ -78,9 +78,11 @@ leq-right-leq-min-ℕ (succ-ℕ k) (succ-ℕ m) (succ-ℕ n) H =
 is-greatest-lower-bound-min-ℕ :
   (l m : ℕ) → is-greatest-binary-lower-bound-Poset ℕ-Poset l m (min-ℕ l m)
 is-greatest-lower-bound-min-ℕ l m =
-  ( leq-left-leq-min-ℕ (min-ℕ l m) l m (refl-leq-ℕ (min-ℕ l m)),
-    leq-right-leq-min-ℕ (min-ℕ l m) l m (refl-leq-ℕ (min-ℕ l m))),
-  λ x (x≤l , x≤m) → leq-min-ℕ x l m x≤l x≤m
+  prove-is-greatest-binary-lower-bound-Poset
+    ( ℕ-Poset)
+    ( leq-left-leq-min-ℕ (min-ℕ l m) l m (refl-leq-ℕ (min-ℕ l m)) ,
+      leq-right-leq-min-ℕ (min-ℕ l m) l m (refl-leq-ℕ (min-ℕ l m)))
+    ( λ x (H , K) → leq-min-ℕ x l m H K)
 ```
 
 ### Associativity of `min-ℕ`

src/elementary-number-theory/minimum-standard-finite-types.lagda.md

@@ -85,10 +85,18 @@ leq-right-leq-min-Fin (succ-ℕ k) (inr x) (inr x₁) (inl x₂) p = p
 is-greatest-lower-bound-min-Fin :
   (k : ℕ) (l m : Fin k) →
   is-greatest-binary-lower-bound-Poset (Fin-Poset k) l m (min-Fin k l m)
-pr1 (pr1 (is-greatest-lower-bound-min-Fin k l m)) =
-  leq-left-leq-min-Fin k (min-Fin k l m) l m (refl-leq-Fin k (min-Fin k l m))
-pr2 (pr1 (is-greatest-lower-bound-min-Fin k l m)) =
-  leq-right-leq-min-Fin k (min-Fin k l m) l m (refl-leq-Fin k (min-Fin k l m))
-pr2 (is-greatest-lower-bound-min-Fin k l m) x (pair H K) =
-  leq-min-Fin k x l m H K
+is-greatest-lower-bound-min-Fin k l m =
+  prove-is-greatest-binary-lower-bound-Poset
+    ( Fin-Poset k)
+    ( ( leq-left-leq-min-Fin k
+        ( min-Fin k l m)
+        ( l)
+        ( m)
+        ( refl-leq-Fin k (min-Fin k l m))) ,
+      ( leq-right-leq-min-Fin k
+        ( min-Fin k l m)
+        ( l)
+        ( m)
+        ( refl-leq-Fin k (min-Fin k l m))))
+    ( λ x (H , K) → leq-min-Fin k x l m H K)
 ```

src/group-theory.lagda.md

@@ -79,6 +79,7 @@ open import group-theory.isomorphisms-groups public
 open import group-theory.isomorphisms-semigroups public
 open import group-theory.kernels public
 open import group-theory.kernels-homomorphisms-concrete-groups public
+open import group-theory.large-semigroups public
 open import group-theory.loop-groups-sets public
 open import group-theory.mere-equivalences-concrete-group-actions public
 open import group-theory.mere-equivalences-group-actions public

src/group-theory/large-semigroups.lagda.md

@@ -0,0 +1,65 @@
+# Large semigroups
+
+```agda
+module group-theory.large-semigroups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A **large semigroup** with universe indexing function `α : Level → Level`
+consists of:
+
+- For each universe level `l` a set `X l : UU (α l)`
+- For any two universe levels `l1` and `l2` a binary operation
+  `μ l1 l2 : X l1 → X l2 → X (l1 ⊔ l2)` satisfying the following associativity
+  law:
+
+```md
+  μ (l1 ⊔ l2) l3 (μ l1 l2 x y) z ＝ μ l1 (l2 ⊔ l3) x (μ l2 l3 y z).
+```
+
+## Definitions
+
+```agda
+record Large-Semigroup (α : Level → Level) : UUω where
+  constructor
+    make-Large-Semigroup
+  field
+    set-Large-Semigroup :
+      (l : Level) → Set (α l)
+    mul-Large-Semigroup :
+      {l1 l2 : Level} →
+      type-Set (set-Large-Semigroup l1) →
+      type-Set (set-Large-Semigroup l2) →
+      type-Set (set-Large-Semigroup (l1 ⊔ l2))
+    associative-mul-Large-Semigroup :
+      {l1 l2 l3 : Level}
+      (x : type-Set (set-Large-Semigroup l1))
+      (y : type-Set (set-Large-Semigroup l2))
+      (z : type-Set (set-Large-Semigroup l3)) →
+      mul-Large-Semigroup (mul-Large-Semigroup x y) z ＝
+      mul-Large-Semigroup x (mul-Large-Semigroup y z)
+
+open Large-Semigroup public
+
+module _
+  {α : Level → Level} (G : Large-Semigroup α)
+  where
+
+  type-Large-Semigroup : (l : Level) → UU (α l)
+  type-Large-Semigroup l = type-Set (set-Large-Semigroup G l)
+
+  is-set-type-Large-Semigroup :
+    {l : Level} → is-set (type-Large-Semigroup l)
+  is-set-type-Large-Semigroup = is-set-type-Set (set-Large-Semigroup G _)
+```

src/order-theory.lagda.md

@@ -30,6 +30,7 @@ open import order-theory.ideals-preorders public
 open import order-theory.infinite-distributive-law public
 open import order-theory.interval-subposets public
 open import order-theory.join-semilattices public
+open import order-theory.large-meet-semilattices public
 open import order-theory.large-posets public
 open import order-theory.large-preorders public
 open import order-theory.largest-elements-posets public
@@ -39,6 +40,7 @@ open import order-theory.least-elements-posets public
 open import order-theory.least-elements-preorders public
 open import order-theory.least-upper-bounds-posets public
 open import order-theory.locally-finite-posets public
+open import order-theory.lower-bounds-posets public
 open import order-theory.lower-types-preorders public
 open import order-theory.maximal-chains-posets public
 open import order-theory.maximal-chains-preorders public

src/order-theory/distributive-lattices.lagda.md

@@ -117,7 +117,7 @@ module _
   is-meet-semilattice-Distributive-Lattice =
     is-meet-semilattice-Lattice lattice-Distributive-Lattice
 
-  meet-semilattice-Distributive-Lattice : Meet-Semilattice l1 l2
+  meet-semilattice-Distributive-Lattice : Meet-Semilattice l1
   meet-semilattice-Distributive-Lattice =
     meet-semilattice-Lattice lattice-Distributive-Lattice
 
@@ -131,7 +131,7 @@ module _
   is-join-semilattice-Distributive-Lattice =
     is-join-semilattice-Lattice lattice-Distributive-Lattice
 
-  join-semilattice-Distributive-Lattice : Join-Semilattice l1 l2
+  join-semilattice-Distributive-Lattice : Join-Semilattice l1
   join-semilattice-Distributive-Lattice =
     join-semilattice-Lattice lattice-Distributive-Lattice
 

src/order-theory/finitely-graded-posets.lagda.md

@@ -39,7 +39,7 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-A finitely graded poset consists of a family of types indexed by
+A **finitely graded poset** consists of a family of types indexed by
 `Fin (succ-ℕ k)` equipped with an ordering relation from `Fin (inl i)` to
 `Fin (succ-Fin (inl i))` for each `i : Fin k`.
 

src/order-theory/frames.lagda.md

@@ -23,35 +23,35 @@ open import order-theory.suplattices
 
 ## Idea
 
-A frame is a poset that has binary meets and arbitrary joins and further
-satisfies the infinite distributive law.
+A **frame** is a meet-semilattice with arbitrary joins, such that meets
+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.
 
 ```agda
-Frame : (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
-Frame l1 l2 l3 =
-  Σ (Meet-Suplattice l1 l2 l3) (distributive-law-meet-suplattice l1 l2 l3)
+Frame : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Frame l1 l2 =
+  Σ (Meet-Suplattice l1 l2) (distributive-law-meet-suplattice l1 l2)
 ```
 
 ## Now we retrieve all the information from a frame (i.e. break up all of it's components, etc.)
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (A : Frame l1 l2 l3)
+  {l1 l2 : Level} (A : Frame l1 l2)
   where
 
-  poset-Frame : Poset l1 l2
+  poset-Frame : Poset l1 l1
   poset-Frame = poset-Meet-Suplattice (pr1 A)
 
   type-Frame : UU l1
   type-Frame = type-Poset poset-Frame
 
-  leq-Frame-Prop : (x y : type-Frame) → Prop l2
+  leq-Frame-Prop : (x y : type-Frame) → Prop l1
   leq-Frame-Prop = leq-Poset-Prop poset-Frame
 
-  leq-Frame : (x y : type-Frame) → UU l2
+  leq-Frame : (x y : type-Frame) → UU l1
   leq-Frame = leq-Poset poset-Frame
 
   is-prop-leq-Frame :
@@ -79,44 +79,35 @@ module _
   set-Frame : Set l1
   set-Frame = set-Poset poset-Frame
 
-  is-meet-semilattice-Frame :
-    is-meet-semilattice-Poset poset-Frame
-  is-meet-semilattice-Frame = is-meet-semilattice-Meet-Suplattice (pr1 A)
-
-  meet-semilattice-Frame : Meet-Semilattice l1 l2
-  meet-semilattice-Frame = ( poset-Frame , is-meet-semilattice-Frame)
+  meet-semilattice-Frame : Meet-Semilattice l1
+  meet-semilattice-Frame = meet-semilattice-Meet-Suplattice (pr1 A)
 
   is-suplattice-Frame :
-    is-suplattice-Poset l3 poset-Frame
+    is-suplattice-Poset l2 poset-Frame
   is-suplattice-Frame = is-suplattice-Meet-Suplattice (pr1 A)
 
-  suplattice-Frame : Suplattice l1 l2 l3
+  suplattice-Frame : Suplattice l1 l1 l2
   suplattice-Frame = ( poset-Frame , is-suplattice-Frame)
 
   meet-suplattice-Frame :
-    Meet-Suplattice l1 l2 l3
-  pr1 meet-suplattice-Frame =
-    poset-Frame
-  pr1 (pr2 meet-suplattice-Frame) =
-    is-meet-semilattice-Frame
-  pr2 (pr2 meet-suplattice-Frame) =
-    is-suplattice-Frame
+    Meet-Suplattice l1 l2
+  meet-suplattice-Frame = pr1 A
 
   meet-Frame :
     (x y : type-Frame) →
     type-Frame
-  meet-Frame x y = pr1 (is-meet-semilattice-Frame x y)
+  meet-Frame = meet-Meet-Semilattice meet-semilattice-Frame
 
   sup-Frame :
-    (I : UU l3) → (I → type-Frame) →
+    (I : UU l2) → (I → type-Frame) →
     type-Frame
   sup-Frame I b = pr1 (is-suplattice-Frame I b)
 
   distributive-law-Frame :
-    distributive-law-meet-suplattice l1 l2 l3 meet-suplattice-Frame
+    distributive-law-meet-suplattice l1 l2 meet-suplattice-Frame
   distributive-law-Frame = pr2 A
 
-  frame-Frame : Frame l1 l2 l3
+  frame-Frame : Frame l1 l2
   pr1 frame-Frame = meet-suplattice-Frame
   pr2 frame-Frame = distributive-law-Frame
 ```

src/order-theory/galois-connections.lagda.md

@@ -41,7 +41,7 @@ module _
   where
 
   adjoint-relation-galois-connection-Prop :
-    hom-Poset P Q → hom-Poset Q P → Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+    type-hom-Poset P Q → type-hom-Poset Q P → Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   adjoint-relation-galois-connection-Prop f g =
     Π-Prop
       ( type-Poset P)
@@ -54,24 +54,24 @@ module _
               ( leq-Poset-Prop P x (map-hom-Poset Q P g y))))
 
   is-lower-adjoint-Galois-Connection :
-    hom-Poset P Q → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+    type-hom-Poset P Q → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   is-lower-adjoint-Galois-Connection f =
     type-subtype (adjoint-relation-galois-connection-Prop f)
 
   is-upper-adjoint-Galois-Connection :
-    hom-Poset Q P → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+    type-hom-Poset Q P → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   is-upper-adjoint-Galois-Connection g =
     type-subtype (λ f → adjoint-relation-galois-connection-Prop f g)
 
   Galois-Connection : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   Galois-Connection =
-    Σ ( hom-Poset Q P) is-upper-adjoint-Galois-Connection
+    Σ ( type-hom-Poset Q P) is-upper-adjoint-Galois-Connection
 
   module _
     (G : Galois-Connection)
     where
 
-    upper-adjoint-Galois-Connection : hom-Poset Q P
+    upper-adjoint-Galois-Connection : type-hom-Poset Q P
     upper-adjoint-Galois-Connection = pr1 G
 
     map-upper-adjoint-Galois-Connection :
@@ -88,7 +88,7 @@ module _
       is-upper-adjoint-Galois-Connection upper-adjoint-Galois-Connection
     is-upper-adjoint-upper-adjoint-Galois-Connection = pr2 G
 
-    lower-adjoint-Galois-Connection : hom-Poset P Q
+    lower-adjoint-Galois-Connection : type-hom-Poset P Q
     lower-adjoint-Galois-Connection =
       pr1 is-upper-adjoint-upper-adjoint-Galois-Connection
 
@@ -137,7 +137,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4) (f : hom-Poset P Q)
+  {l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4)
+  (f : type-hom-Poset P Q)
   where
 
   htpy-is-lower-adjoint-Galois-Connection :
@@ -205,7 +206,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4) (g : hom-Poset Q P)
+  {l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4)
+  (g : type-hom-Poset Q P)
   where
 
   htpy-is-upper-adjoint-Galois-Connection :