update contributors, remove unused imports (#772)

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)

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
 ```

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

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

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
 ```

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
 ```

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

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

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

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

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
 ```

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>

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

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

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>

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>

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
 ```

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>

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>

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

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>

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

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

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
 

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
 

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

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

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

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
 

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

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
 

src/order-theory/large-meet-semilattices.lagda.md

@@ -8,7 +8,6 @@ module order-theory.large-meet-semilattices where
 
 ```agda
 open import foundation.action-on-identifications-binary-functions
-open import foundation.binary-relations
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.large-binary-relations