Subframes and quotient locales via nuclei (UniMath#613)

fredrik-bakke · May 20, 2023 · ee5a96c · ee5a96c
1 parent 750f151
commit ee5a96c
Show file tree

Hide file tree

Showing 9 changed files with 18 additions and 0 deletions.
diff --git a/src/foundation/large-locale-of-propositions.lagda.md b/src/foundation/large-locale-of-propositions.lagda.md
@@ -16,6 +16,7 @@ open import foundation-core.functions
 open import foundation-core.propositions
 open import foundation-core.universe-levels
 
+open import order-theory.greatest-lower-bounds-large-posets
 open import order-theory.large-frames
 open import order-theory.large-locales
 open import order-theory.large-meet-semilattices

diff --git a/src/order-theory/dependent-products-large-locales.lagda.md b/src/order-theory/dependent-products-large-locales.lagda.md
@@ -13,7 +13,11 @@ open import foundation.sets
 open import foundation.universe-levels
 
 open import order-theory.dependent-products-large-frames
+open import order-theory.dependent-products-large-meet-semilattices
+open import order-theory.dependent-products-large-posets
+open import order-theory.dependent-products-large-suplattices
 open import order-theory.greatest-lower-bounds-large-posets
+open import order-theory.large-frames
 open import order-theory.large-locales
 open import order-theory.large-meet-semilattices
 open import order-theory.large-posets

diff --git a/src/order-theory/homomorphisms-large-frames.lagda.md b/src/order-theory/homomorphisms-large-frames.lagda.md
@@ -7,12 +7,14 @@ module order-theory.homomorphisms-large-frames where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.functions
 open import foundation.identity-types
 open import foundation.universe-levels
 
 open import order-theory.homomorphisms-large-meet-semilattices
 open import order-theory.homomorphisms-large-suplattices
 open import order-theory.large-frames
+open import order-theory.order-preserving-maps-large-posets
 ```
 
 </details>

diff --git a/src/order-theory/large-meet-semilattices.lagda.md b/src/order-theory/large-meet-semilattices.lagda.md
@@ -13,6 +13,7 @@ open import foundation.universe-levels
 
 open import order-theory.greatest-lower-bounds-large-posets
 open import order-theory.large-posets
+open import order-theory.lower-bounds-large-posets
 open import order-theory.top-elements-large-posets
 ```
 

diff --git a/src/order-theory/large-meet-subsemilattices.lagda.md b/src/order-theory/large-meet-subsemilattices.lagda.md
@@ -10,6 +10,7 @@ module order-theory.large-meet-subsemilattices where
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
+open import foundation.sets
 open import foundation.universe-levels
 
 open import order-theory.greatest-lower-bounds-large-posets

diff --git a/src/order-theory/large-quotient-locales.lagda.md b/src/order-theory/large-quotient-locales.lagda.md
@@ -7,6 +7,8 @@ module order-theory.large-quotient-locales where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.dependent-pair-types
+open import foundation.functions
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.universe-levels

diff --git a/src/order-theory/large-subposets.lagda.md b/src/order-theory/large-subposets.lagda.md
@@ -10,6 +10,7 @@ module order-theory.large-subposets where
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
+open import foundation.sets
 open import foundation.subtypes
 open import foundation.universe-levels
 

diff --git a/src/order-theory/large-subsuplattices.lagda.md b/src/order-theory/large-subsuplattices.lagda.md
@@ -7,11 +7,14 @@ module order-theory.large-subsuplattices where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
+open import foundation.subtypes
 open import foundation.universe-levels
 
 open import order-theory.large-posets
+open import order-theory.large-preorders
 open import order-theory.large-subposets
 open import order-theory.large-suplattices
 ```

diff --git a/src/order-theory/nuclei-large-locales.lagda.md b/src/order-theory/nuclei-large-locales.lagda.md
@@ -22,8 +22,11 @@ open import order-theory.large-locales
 open import order-theory.large-meet-semilattices
 open import order-theory.large-meet-subsemilattices
 open import order-theory.large-posets
+open import order-theory.large-quotient-locales
+open import order-theory.large-subframes
 open import order-theory.large-subposets
 open import order-theory.large-subpreorders
+open import order-theory.large-subsuplattices
 open import order-theory.large-suplattices
 open import order-theory.least-upper-bounds-large-posets
 ```