UniMath · EgbertRijke · Sep 15, 2023 · Sep 15, 2023 · Sep 15, 2023 · Sep 15, 2023
diff --git a/CONTRIBUTORS.md b/CONTRIBUTORS.md
@@ -11,18 +11,19 @@ We are grateful to the following people for their contributions to the library.
 - [Raymond Baker](https://github.com/morphismz)
 - [ElifUskuplu](https://github.com/ElifUskuplu)
 - [VictorBlanchi](https://github.com/VictorBlanchi)
+- [Vojtěch Štěpančík](https://github.com/VojtechStep)
 - [IanRay11](https://github.com/IanRay11)
 - [Andreas Källberg](https://github.com/anka-213)
 - [Matej Jazbec](https://github.com/MatejJazbec)
 - [malarbol](https://github.com/malarbol)
 - [Amélia](https://github.com/plt-amy)
 - [ivankobe](https://github.com/ivankobe)
 - [daniel gratzer](https://github.com/jozefg)
-- [Vojtěch Štěpančík](https://github.com/VojtechStep)
 - [Fernando Chu](https://github.com/FernandoChu)
 - [Alice Laroche](https://github.com/Seiryn21)
 - [masazaucer](https://github.com/masazaucer)
 - [favonia](https://github.com/favonia)
+- [maybemabeline](https://github.com/maybemabeline)
 - [Szumi Xie](https://github.com/szumixie)
 - [Åsmund Kløvstad](https://github.com/Aqissiaq)
 - [Dylan Braithwaite](https://github.com/dylanbraithwaite)
@@ -31,7 +32,6 @@ We are grateful to the following people for their contributions to the library.
 - [Matthias Hutzler](https://github.com/MatthiasHu)
 - [Nathan van Doorn](https://github.com/Taneb)
 - [Pierre Cagne](https://github.com/pierrecagne)
-- [Tom de Jong](https://github.com/tomdjong)
 
 Help us to improve the library by contributing to the project! Contributions
 come in many forms, please ask us if you are not sure how to help. We are happy

diff --git a/src/category-theory/anafunctors-categories.lagda.md b/src/category-theory/anafunctors-categories.lagda.md
@@ -10,14 +10,8 @@ module category-theory.anafunctors-categories where
 open import category-theory.anafunctors-precategories
 open import category-theory.categories
 open import category-theory.functors-categories
-open import category-theory.functors-precategories
-open import category-theory.isomorphisms-in-precategories
-open import category-theory.precategories
 
-open import foundation.action-on-identifications-functions
-open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
-open import foundation.identity-types
 open import foundation.propositional-truncations
 open import foundation.universe-levels
 ```

diff --git a/src/category-theory/anafunctors-precategories.lagda.md b/src/category-theory/anafunctors-precategories.lagda.md
@@ -7,7 +7,6 @@ module category-theory.anafunctors-precategories where
 <details><summary>Imports</summary>
 
 ```agda
-open import category-theory.categories
 open import category-theory.functors-precategories
 open import category-theory.isomorphisms-in-precategories
 open import category-theory.precategories

diff --git a/src/category-theory/endomorphisms-in-categories.lagda.md b/src/category-theory/endomorphisms-in-categories.lagda.md
@@ -10,7 +10,6 @@ module category-theory.endomorphisms-in-categories where
 open import category-theory.categories
 open import category-theory.endomorphisms-in-precategories
 
-open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.sets
 open import foundation.universe-levels

diff --git a/src/commutative-algebra/poset-of-ideals-commutative-rings.lagda.md b/src/commutative-algebra/poset-of-ideals-commutative-rings.lagda.md
@@ -16,7 +16,6 @@ open import foundation.universe-levels
 
 open import order-theory.large-posets
 open import order-theory.large-preorders
-open import order-theory.similarity-of-elements-large-posets
 
 open import ring-theory.poset-of-ideals-rings
 ```

diff --git a/src/elementary-number-theory/multiplication-integer-fractions.lagda.md b/src/elementary-number-theory/multiplication-integer-fractions.lagda.md
@@ -7,13 +7,10 @@ module elementary-number-theory.multiplication-integer-fractions where
 <details><summary>Imports</summary>
 
 ```agda
-open import elementary-number-theory.addition-integers
 open import elementary-number-theory.integer-fractions
-open import elementary-number-theory.integers
 open import elementary-number-theory.multiplication-integers
 
 open import foundation.action-on-identifications-binary-functions
-open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 ```

diff --git a/src/elementary-number-theory/multiplication-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-rational-numbers.lagda.md
@@ -10,10 +10,8 @@ module elementary-number-theory.multiplication-rational-numbers where
 
 ```agda
 open import elementary-number-theory.integer-fractions
-open import elementary-number-theory.integers
 open import elementary-number-theory.multiplication-integer-fractions
 open import elementary-number-theory.rational-numbers
-open import elementary-number-theory.reduced-integer-fractions
 
 open import foundation.dependent-pair-types
 open import foundation.identity-types

diff --git a/src/foundation/category-of-sets.lagda.md b/src/foundation/category-of-sets.lagda.md
@@ -9,7 +9,6 @@ module foundation.category-of-sets where
 ```agda
 open import category-theory.categories
 open import category-theory.isomorphisms-in-large-precategories
-open import category-theory.isomorphisms-in-precategories
 open import category-theory.large-categories
 open import category-theory.large-precategories
 open import category-theory.precategories

diff --git a/src/foundation/fibered-equivalences.lagda.md b/src/foundation/fibered-equivalences.lagda.md
@@ -7,7 +7,6 @@ module foundation.fibered-equivalences where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equivalences

diff --git a/src/foundation/functoriality-dependent-function-types.lagda.md b/src/foundation/functoriality-dependent-function-types.lagda.md
@@ -13,7 +13,6 @@ open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equivalence-extensionality
 open import foundation.function-extensionality
-open import foundation.homotopy-induction
 open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universal-property-unit-type

diff --git a/src/foundation/homotopies.lagda.md b/src/foundation/homotopies.lagda.md
@@ -21,8 +21,6 @@ open import foundation.universe-levels
 open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-function-types
-open import foundation-core.functoriality-dependent-pair-types
-open import foundation-core.sections
 open import foundation-core.transport-along-identifications
 open import foundation-core.whiskering-homotopies
 ```

diff --git a/src/foundation/homotopy-induction.lagda.md b/src/foundation/homotopy-induction.lagda.md
@@ -8,17 +8,14 @@ module foundation.homotopy-induction where
 
 ```agda
 open import foundation.dependent-pair-types
-open import foundation.equivalence-extensionality
 open import foundation.function-extensionality
 open import foundation.identity-systems
 open import foundation.universe-levels
 
 open import foundation-core.contractible-types
-open import foundation-core.equivalences
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
-open import foundation-core.sections
 ```
 
 </details>

diff --git a/src/foundation/images.lagda.md b/src/foundation/images.lagda.md
@@ -21,8 +21,6 @@ open import foundation-core.contractible-types
 open import foundation-core.embeddings
 open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
-open import foundation-core.function-types
-open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.injective-maps
 open import foundation-core.propositions

diff --git a/src/foundation/large-locale-of-subtypes.lagda.md b/src/foundation/large-locale-of-subtypes.lagda.md
@@ -12,7 +12,6 @@ open import foundation.large-locale-of-propositions
 open import foundation.universe-levels
 
 open import foundation-core.identity-types
-open import foundation-core.propositions
 open import foundation-core.sets
 
 open import order-theory.greatest-lower-bounds-large-posets

diff --git a/src/foundation/sigma-closed-subuniverses.lagda.md b/src/foundation/sigma-closed-subuniverses.lagda.md
@@ -12,7 +12,6 @@ open import foundation.subuniverses
 open import foundation.universe-levels
 
 open import foundation-core.function-types
-open import foundation-core.propositions
 ```
 
 </details>

diff --git a/src/foundation/symmetric-cores-binary-relations.lagda.md b/src/foundation/symmetric-cores-binary-relations.lagda.md
@@ -9,28 +9,17 @@ module foundation.symmetric-cores-binary-relations where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.action-on-identifications-functions
 open import foundation.binary-relations
-open import foundation.dependent-pair-types
 open import foundation.equivalences
-open import foundation.function-extensionality
-open import foundation.function-types
 open import foundation.functoriality-dependent-function-types
 open import foundation.functoriality-function-types
-open import foundation.homotopies
-open import foundation.identity-types
-open import foundation.mere-equivalences
 open import foundation.symmetric-binary-relations
 open import foundation.transport-along-identifications
 open import foundation.type-arithmetic-dependent-function-types
-open import foundation.universal-property-dependent-pair-types
-open import foundation.universal-property-identity-systems
 open import foundation.universe-levels
 open import foundation.unordered-pairs
 
-open import univalent-combinatorics.2-element-types
 open import univalent-combinatorics.standard-finite-types
-open import univalent-combinatorics.universal-property-standard-finite-types
 ```
 
 </details>

diff --git a/src/group-theory/centralizer-subgroups.lagda.md b/src/group-theory/centralizer-subgroups.lagda.md
@@ -17,7 +17,6 @@ open import foundation.universe-levels
 
 open import group-theory.conjugation
 open import group-theory.groups
-open import group-theory.normal-subgroups
 open import group-theory.subgroups
 open import group-theory.subsets-groups
 ```

diff --git a/src/group-theory/conjugation-concrete-groups.lagda.md b/src/group-theory/conjugation-concrete-groups.lagda.md
@@ -16,8 +16,6 @@ open import group-theory.conjugation
 open import group-theory.homomorphisms-concrete-groups
 
 open import higher-group-theory.conjugation
-
-open import synthetic-homotopy-theory.conjugation-loops
 ```
 
 </details>

diff --git a/src/group-theory/cyclic-groups.lagda.md b/src/group-theory/cyclic-groups.lagda.md
@@ -8,26 +8,18 @@ module group-theory.cyclic-groups where
 
 ```agda
 open import foundation.dependent-pair-types
-open import foundation.embeddings
 open import foundation.existential-quantification
 open import foundation.identity-types
 open import foundation.inhabited-subtypes
 open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.sets
 open import foundation.subtypes
-open import foundation.surjective-maps
 open import foundation.universe-levels
 
 open import group-theory.abelian-groups
-open import group-theory.addition-homomorphisms-abelian-groups
-open import group-theory.free-groups-with-one-generator
-open import group-theory.full-subgroups
 open import group-theory.generating-elements-groups
 open import group-theory.groups
-open import group-theory.homomorphisms-abelian-groups
-open import group-theory.homomorphisms-groups
-open import group-theory.subgroups-generated-by-elements-groups
 ```
 
 </details>

diff --git a/src/group-theory/generating-elements-groups.lagda.md b/src/group-theory/generating-elements-groups.lagda.md
@@ -10,10 +10,8 @@ module group-theory.generating-elements-groups where
 open import commutative-algebra.commutative-rings
 
 open import elementary-number-theory.integers
-open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions
-open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equivalences
@@ -37,15 +35,12 @@ open import group-theory.endomorphism-rings-abelian-groups
 open import group-theory.free-groups-with-one-generator
 open import group-theory.full-subgroups
 open import group-theory.groups
-open import group-theory.homomorphisms-abelian-groups
 open import group-theory.homomorphisms-groups
-open import group-theory.images-of-group-homomorphisms
 open import group-theory.integer-multiples-of-elements-abelian-groups
 open import group-theory.integer-powers-of-elements-groups
 open import group-theory.isomorphisms-abelian-groups
 open import group-theory.normal-subgroups
 open import group-theory.quotient-groups
-open import group-theory.subgroups
 open import group-theory.subgroups-generated-by-elements-groups
 open import group-theory.subsets-groups
 open import group-theory.trivial-group-homomorphisms

diff --git a/src/group-theory/representations-monoids.lagda.md b/src/group-theory/representations-monoids.lagda.md
@@ -11,15 +11,11 @@ open import category-theory.categories
 open import category-theory.endomorphisms-in-categories
 
 open import foundation.dependent-pair-types
-open import foundation.endomorphisms
 open import foundation.identity-types
 open import foundation.universe-levels
 
 open import group-theory.homomorphisms-monoids
 open import group-theory.monoids
-
-open import structured-types.morphisms-wild-monoids
-open import structured-types.wild-monoids
 ```
 
 </details>

diff --git a/src/order-theory/closure-operators-large-locales.lagda.md b/src/order-theory/closure-operators-large-locales.lagda.md
@@ -8,7 +8,6 @@ module order-theory.closure-operators-large-locales where
 
 ```agda
 open import foundation.action-on-identifications-functions
-open import foundation.binary-relations
 open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.identity-types

diff --git a/src/order-theory/closure-operators-large-posets.lagda.md b/src/order-theory/closure-operators-large-posets.lagda.md
@@ -7,7 +7,6 @@ module order-theory.closure-operators-large-posets where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.binary-relations
 open import foundation.function-types
 open import foundation.identity-types
 open import foundation.large-binary-relations

diff --git a/src/order-theory/dependent-products-large-frames.lagda.md b/src/order-theory/dependent-products-large-frames.lagda.md
@@ -7,11 +7,9 @@ module order-theory.dependent-products-large-frames where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.binary-relations
 open import foundation.function-extensionality
 open import foundation.identity-types
 open import foundation.large-binary-relations
-open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
 

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

diff --git a/src/order-theory/dependent-products-large-meet-semilattices.lagda.md b/src/order-theory/dependent-products-large-meet-semilattices.lagda.md
@@ -7,8 +7,6 @@ module order-theory.dependent-products-large-meet-semilattices where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.binary-relations
-open import foundation.identity-types
 open import foundation.large-binary-relations
 open import foundation.sets
 open import foundation.universe-levels

diff --git a/src/order-theory/dependent-products-large-posets.lagda.md b/src/order-theory/dependent-products-large-posets.lagda.md
@@ -7,11 +7,8 @@ module order-theory.dependent-products-large-posets where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.binary-relations
 open import foundation.function-extensionality
-open import foundation.identity-types
 open import foundation.large-binary-relations
-open import foundation.propositions
 open import foundation.universe-levels
 
 open import order-theory.dependent-products-large-preorders

diff --git a/src/order-theory/dependent-products-large-preorders.lagda.md b/src/order-theory/dependent-products-large-preorders.lagda.md
@@ -7,7 +7,6 @@ module order-theory.dependent-products-large-preorders where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.binary-relations
 open import foundation.large-binary-relations
 open import foundation.propositions
 open import foundation.universe-levels

diff --git a/src/order-theory/dependent-products-large-suplattices.lagda.md b/src/order-theory/dependent-products-large-suplattices.lagda.md
@@ -7,10 +7,7 @@ module order-theory.dependent-products-large-suplattices where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.binary-relations
-open import foundation.identity-types
 open import foundation.large-binary-relations
-open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
 

diff --git a/src/order-theory/large-frames.lagda.md b/src/order-theory/large-frames.lagda.md
@@ -7,23 +7,19 @@ module order-theory.large-frames where
 <details><summary>Imports</summary>
 
 ```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

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