Small constructions from large ones in order theory (#680)

Defines
- small semigroups from large semigroups
- small preorders from large preorders
- small posets from large posets
- small suplattices from large suplattices
- small meet semilattices from large meet semilattices
- large preorders are large precategories
- large posets are large categories

src/foundation/univalence-implies-function-extensionality.lagda.md

@@ -27,7 +27,8 @@ open import foundation-core.transport
 
 ## Idea
 
-The univalence axiom implies function extensionality
+The [univalence axiom](foundation-core.univalence.md) implies
+[function extensionality](foundation-core.function-extensionality.md).
 
 ## Theorem
 
@@ -51,5 +52,5 @@ abstract
   funext-univalence :
     {l : Level} {A : UU l} {B : A → UU l} (f : (x : A) → B x) → FUNEXT f
   funext-univalence {A = A} {B} f =
-    FUNEXT-WEAK-FUNEXT (λ A B → weak-funext-univalence) A B f
+    funext-weak-funext (λ A B → weak-funext-univalence) A B f
 ```

src/foundation/universe-levels.lagda.md

@@ -1,8 +1,6 @@
 # Universe levels
 
 ```agda
-{-# OPTIONS --no-import-sorts #-}
-
 module foundation.universe-levels where
 
 open import Agda.Primitive
@@ -15,4 +13,5 @@ open import Agda.Primitive
 
 We import Agda's built in mechanism of universe levels. The universes are called
 `UU`, which stands for _univalent universe_, although we will not immediately
-assume that universes are univalent.
+assume that universes are univalent. This is done in
+[foundation.univalence](foundation.univalence.md).

src/foundation/weak-function-extensionality.lagda.md

@@ -20,6 +20,7 @@ open import foundation-core.empty-types
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
 open import foundation-core.function-extensionality
+open import foundation-core.function-types
 open import foundation-core.identity-types
 open import foundation-core.propositions
 ```
@@ -28,9 +29,10 @@ open import foundation-core.propositions
 
 ## Idea
 
-Weak function extensionality is the principle that any dependent product of
-contractible types is contractible. This principle is equivalent to the function
-extensionality axiom.
+**Weak function extensionality** is the principle that any dependent product of
+[contractible types](foundation-core.contractible-types.md) is contractible.
+This principle is [equivalent](foundation-core.equivalences.md) to
+[the function extensionality axiom](foundation-core.function-extensionality.md).
 
 ## Definition
 
@@ -58,30 +60,29 @@ WEAKER-FUNEXT A B =
 
 ```agda
 abstract
-  WEAK-FUNEXT-FUNEXT :
+  weak-funext-funext :
     {l1 l2 : Level} →
     ((A : UU l1) (B : A → UU l2) (f : (x : A) → B x) → FUNEXT f) →
     ((A : UU l1) (B : A → UU l2) → WEAK-FUNEXT A B)
-  pr1 (WEAK-FUNEXT-FUNEXT funext A B is-contr-B) x = center (is-contr-B x)
-  pr2 (WEAK-FUNEXT-FUNEXT funext A B is-contr-B) f =
-    map-inv-is-equiv (funext A B c f) (λ x → contraction (is-contr-B x) (f x))
-    where
-    c : (x : A) → B x
-    c x = center (is-contr-B x)
+  pr1 (weak-funext-funext funext A B is-contr-B) x =
+    center (is-contr-B x)
+  pr2 (weak-funext-funext funext A B is-contr-B) f =
+    map-inv-is-equiv
+      ( funext A B (λ x → center (is-contr-B x)) f)
+      ( λ x → contraction (is-contr-B x) (f x))
 
 abstract
-  FUNEXT-WEAK-FUNEXT :
+  funext-weak-funext :
     {l1 l2 : Level} →
     ((A : UU l1) (B : A → UU l2) → WEAK-FUNEXT A B) →
     ((A : UU l1) (B : A → UU l2) (f : (x : A) → B x) → FUNEXT f)
-  FUNEXT-WEAK-FUNEXT weak-funext A B f =
+  funext-weak-funext weak-funext A B f =
     fundamental-theorem-id
       ( is-contr-retract-of
         ( (x : A) → Σ (B x) (λ b → f x ＝ b))
-        ( pair
-          ( λ t x → pair (pr1 t x) (pr2 t x))
-          ( pair (λ t → pair (λ x → pr1 (t x)) (λ x → pr2 (t x)))
-          ( λ t → eq-pair-Σ refl refl)))
+        ( ( λ t x → (pr1 t x , pr2 t x)) ,
+          ( λ t → (pr1 ∘ t , pr2 ∘ t)) ,
+          ( λ t → eq-pair-Σ refl refl))
         ( weak-funext A
           ( λ x → Σ (B x) (λ b → f x ＝ b))
           ( λ x → is-contr-total-path (f x))))
@@ -91,43 +92,48 @@ abstract
 ### A partial converse to weak function extensionality
 
 ```agda
-cases-function-converse-weak-funext :
-  {l1 l2 : Level} {I : UU l1} {A : I → UU l2} (d : has-decidable-equality I)
-  (H : is-contr ((i : I) → A i)) (i : I) (x : A i)
-  (j : I) (e : is-decidable (i ＝ j)) → A j
-cases-function-converse-weak-funext d H i x .i (inl refl) = x
-cases-function-converse-weak-funext d H i x j (inr f) = center H j
-
-function-converse-weak-funext :
-  {l1 l2 : Level} {I : UU l1} {A : I → UU l2} (d : has-decidable-equality I)
-  (H : is-contr ((i : I) → A i)) (i : I) (x : A i) (j : I) → A j
-function-converse-weak-funext d H i x j =
-  cases-function-converse-weak-funext d H i x j (d i j)
-
-cases-eq-function-converse-weak-funext :
-  {l1 l2 : Level} {I : UU l1} {A : I → UU l2} (d : has-decidable-equality I)
-  (H : is-contr ((i : I) → A i)) (i : I) (x : A i) (e : is-decidable (i ＝ i)) →
-  cases-function-converse-weak-funext d H i x i e ＝ x
-cases-eq-function-converse-weak-funext d H i x (inl p) =
-  ap
-    ( λ t → cases-function-converse-weak-funext d H i x i (inl t))
-    ( eq-is-prop (is-set-has-decidable-equality d i i) {p} {refl})
-cases-eq-function-converse-weak-funext d H i x (inr f) = ex-falso (f refl)
-
-eq-function-converse-weak-funext :
-  {l1 l2 : Level} {I : UU l1} {A : I → UU l2} (d : has-decidable-equality I)
-  (H : is-contr ((i : I) → A i)) (i : I) (x : A i) →
-  function-converse-weak-funext d H i x i ＝ x
-eq-function-converse-weak-funext d H i x =
-  cases-eq-function-converse-weak-funext d H i x (d i i)
-
-converse-weak-funext :
-  {l1 l2 : Level} {I : UU l1} {A : I → UU l2} →
-  has-decidable-equality I → is-contr ((i : I) → A i) → (i : I) → is-contr (A i)
-pr1 (converse-weak-funext d (pair x H) i) = x i
-pr2 (converse-weak-funext d (pair x H) i) y =
-  ( htpy-eq (H (function-converse-weak-funext d (pair x H) i y)) i) ∙
-  ( eq-function-converse-weak-funext d (pair x H) i y)
+module _
+  {l1 l2 : Level} {I : UU l1} {A : I → UU l2}
+  (d : has-decidable-equality I)
+  (H : is-contr ((i : I) → A i))
+  where
+
+  cases-function-converse-weak-funext :
+    (i : I) (x : A i) (j : I) (e : is-decidable (i ＝ j)) → A j
+  cases-function-converse-weak-funext i x .i (inl refl) = x
+  cases-function-converse-weak-funext i x j (inr f) = center H j
+
+  function-converse-weak-funext :
+    (i : I) (x : A i) (j : I) → A j
+  function-converse-weak-funext i x j =
+    cases-function-converse-weak-funext i x j (d i j)
+
+  cases-eq-function-converse-weak-funext :
+    (i : I) (x : A i) (e : is-decidable (i ＝ i)) →
+    cases-function-converse-weak-funext i x i e ＝ x
+  cases-eq-function-converse-weak-funext i x (inl p) =
+    ap
+      ( λ t → cases-function-converse-weak-funext i x i (inl t))
+      ( eq-is-prop
+        ( is-set-has-decidable-equality d i i)
+        { p}
+        { refl})
+  cases-eq-function-converse-weak-funext i x (inr f) =
+    ex-falso (f refl)
+
+  eq-function-converse-weak-funext :
+    (i : I) (x : A i) →
+    function-converse-weak-funext i x i ＝ x
+  eq-function-converse-weak-funext i x =
+    cases-eq-function-converse-weak-funext i x (d i i)
+
+  converse-weak-funext : (i : I) → is-contr (A i)
+  pr1 (converse-weak-funext i) = center H i
+  pr2 (converse-weak-funext i) y =
+    ( htpy-eq
+      ( contraction H (function-converse-weak-funext i y))
+      ( i)) ∙
+    ( eq-function-converse-weak-funext i y)
 ```
 
 ### Weaker function extensionality implies weak function extensionality

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

@@ -7,9 +7,12 @@ module group-theory.large-semigroups where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.sets
 open import foundation.universe-levels
+
+open import group-theory.semigroups
 ```
 
 </details>
@@ -63,3 +66,16 @@ module _
     {l : Level} → is-set (type-Large-Semigroup l)
   is-set-type-Large-Semigroup = is-set-type-Set (set-Large-Semigroup G _)
 ```
+
+### Small semigroups from large semigroups
+
+```agda
+module _
+  {α : Level → Level} (G : Large-Semigroup α)
+  where
+
+  semigroup-Large-Semigroup : (l : Level) → Semigroup (α l)
+  pr1 (semigroup-Large-Semigroup l) = set-Large-Semigroup G l
+  pr1 (pr2 (semigroup-Large-Semigroup l)) = mul-Large-Semigroup G
+  pr2 (pr2 (semigroup-Large-Semigroup l)) = associative-mul-Large-Semigroup G
+```

src/group-theory/semigroups.lagda.md

@@ -18,7 +18,8 @@ open import foundation.universe-levels
 
 ## Idea
 
-Semigroups are sets equipped an associative binary operation.
+**Semigroups** are [sets](foundation-core.sets.md) equipped with an associative
+binary operation.
 
 ## Definition
 
@@ -71,7 +72,7 @@ module _
   associative-mul-Semigroup = pr2 has-associative-mul-Semigroup
 ```
 
-### Equip a type with a structure of semigroup
+### Equip a type with the structure of a semigroup
 
 ```agda
 structure-semigroup :

src/order-theory/large-frames.lagda.md

@@ -8,18 +8,25 @@ module order-theory.large-frames where
 
 ```agda
 open import foundation.binary-relations
+open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.large-binary-relations
 open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
 
+open import order-theory.frames
 open import order-theory.greatest-lower-bounds-large-posets
 open import order-theory.large-meet-semilattices
 open import order-theory.large-posets
 open import order-theory.large-preorders
 open import order-theory.large-suplattices
 open import order-theory.least-upper-bounds-large-posets
+open import order-theory.meet-semilattices
+open import order-theory.meet-suplattices
+open import order-theory.posets
+open import order-theory.preorders
+open import order-theory.suplattices
 open import order-theory.top-elements-large-posets
 open import order-theory.upper-bounds-large-posets
 ```
@@ -28,8 +35,8 @@ open import order-theory.upper-bounds-large-posets
 
 ## Idea
 
-A **large frame** is a large meet-suplattice satisfying the distributive law for
-meets over suprema.
+A **large frame** is a large [meet-suplattice](order-theory.meet-suplattices.md)
+satisfying the distributive law for meets over suprema.
 
 ## Definitions
 
@@ -210,3 +217,52 @@ module _
   is-upper-bound-sup-Large-Frame =
     is-upper-bound-sup-Large-Suplattice large-suplattice-Large-Frame
 ```
+
+## Properties
+
+### Small constructions from large frames
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} {γ : Level}
+  (L : Large-Frame α β γ)
+  where
+
+  preorder-Large-Frame : (l : Level) → Preorder (α l) (β l l)
+  preorder-Large-Frame = preorder-Large-Preorder (large-preorder-Large-Frame L)
+
+  poset-Large-Frame : (l : Level) → Poset (α l) (β l l)
+  poset-Large-Frame = poset-Large-Poset (large-poset-Large-Frame L)
+
+  is-suplattice-poset-Large-Frame :
+    (l1 l2 : Level) → is-suplattice-Poset l1 (poset-Large-Frame (γ ⊔ l1 ⊔ l2))
+  pr1 (is-suplattice-poset-Large-Frame l1 l2 I y) =
+    sup-Large-Frame L y
+  pr2 (is-suplattice-poset-Large-Frame l1 l2 I y) =
+    is-least-upper-bound-sup-Large-Frame L y
+
+  suplattice-Large-Frame :
+    (l1 l2 : Level) →
+    Suplattice (α (γ ⊔ l1 ⊔ l2)) (β (γ ⊔ l1 ⊔ l2) (γ ⊔ l1 ⊔ l2)) l1
+  pr1 (suplattice-Large-Frame l1 l2) = poset-Large-Frame (γ ⊔ l1 ⊔ l2)
+  pr2 (suplattice-Large-Frame l1 l2) = is-suplattice-poset-Large-Frame l1 l2
+
+  is-meet-semilattice-poset-Large-Frame :
+    (l : Level) → is-meet-semilattice-Poset (poset-Large-Frame l)
+  pr1 (is-meet-semilattice-poset-Large-Frame l x y) =
+    meet-Large-Frame L x y
+  pr2 (is-meet-semilattice-poset-Large-Frame l x y) =
+    is-greatest-binary-lower-bound-meet-Large-Frame L x y
+
+  order-theoretic-meet-semilattice-Large-Frame :
+    (l : Level) → Order-Theoretic-Meet-Semilattice (α l) (β l l)
+  pr1 (order-theoretic-meet-semilattice-Large-Frame l) =
+    poset-Large-Frame l
+  pr2 (order-theoretic-meet-semilattice-Large-Frame l) =
+    is-meet-semilattice-poset-Large-Frame l
+
+  meet-semilattice-Large-Frame : (l : Level) → Meet-Semilattice (α l)
+  meet-semilattice-Large-Frame =
+    meet-semilattice-Large-Meet-Semilattice
+      ( large-meet-semilattice-Large-Frame L)
+```

src/order-theory/large-locales.lagda.md

@@ -21,6 +21,10 @@ open import order-theory.large-posets
 open import order-theory.large-preorders
 open import order-theory.large-suplattices
 open import order-theory.least-upper-bounds-large-posets
+open import order-theory.meet-semilattices
+open import order-theory.posets
+open import order-theory.preorders
+open import order-theory.suplattices
 open import order-theory.top-elements-large-posets
 open import order-theory.upper-bounds-large-posets
 ```
@@ -29,8 +33,9 @@ open import order-theory.upper-bounds-large-posets
 
 ## Idea
 
-A **large locale** is a large meet-suplattice satisfying the distributive law
-for meets over suprema.
+A **large locale** is a large
+[meet-suplattice](order-theory.meet-suplattices.md) satisfying the distributive
+law for meets over suprema.
 
 ## Definitions
 
@@ -179,3 +184,42 @@ module _
   distributive-meet-sup-Large-Locale =
     distributive-meet-sup-Large-Frame L
 ```
+
+## Properties
+
+### Small constructions from large locales
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} {γ : Level}
+  (L : Large-Locale α β γ)
+  where
+
+  preorder-Large-Locale : (l : Level) → Preorder (α l) (β l l)
+  preorder-Large-Locale = preorder-Large-Frame L
+
+  poset-Large-Locale : (l : Level) → Poset (α l) (β l l)
+  poset-Large-Locale = poset-Large-Frame L
+
+  is-suplattice-poset-Large-Locale :
+    (l1 l2 : Level) → is-suplattice-Poset l1 (poset-Large-Locale (γ ⊔ l1 ⊔ l2))
+  is-suplattice-poset-Large-Locale = is-suplattice-poset-Large-Frame L
+
+  suplattice-Large-Locale :
+    (l1 l2 : Level) →
+    Suplattice (α (γ ⊔ l1 ⊔ l2)) (β (γ ⊔ l1 ⊔ l2) (γ ⊔ l1 ⊔ l2)) l1
+  suplattice-Large-Locale = suplattice-Large-Frame L
+
+  is-meet-semilattice-poset-Large-Locale :
+    (l : Level) → is-meet-semilattice-Poset (poset-Large-Locale l)
+  is-meet-semilattice-poset-Large-Locale =
+    is-meet-semilattice-poset-Large-Frame L
+
+  order-theoretic-meet-semilattice-Large-Locale :
+    (l : Level) → Order-Theoretic-Meet-Semilattice (α l) (β l l)
+  order-theoretic-meet-semilattice-Large-Locale =
+    order-theoretic-meet-semilattice-Large-Frame L
+
+  meet-semilattice-Large-Locale : (l : Level) → Meet-Semilattice (α l)
+  meet-semilattice-Large-Locale = meet-semilattice-Large-Frame L
+```