diff --git a/CONTRIBUTORS.md b/CONTRIBUTORS.md index 2380cb1b4c..a28fe1a0b6 100644 --- a/CONTRIBUTORS.md +++ b/CONTRIBUTORS.md @@ -11,6 +11,7 @@ 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) @@ -18,11 +19,11 @@ We are grateful to the following people for their contributions to the library. - [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) diff --git a/src/category-theory/anafunctors-categories.lagda.md b/src/category-theory/anafunctors-categories.lagda.md index 5686ea34fb..4cc6b74fba 100644 --- 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 index 1b24705471..360d573988 100644 --- 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
Imports ```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 index 3a9e374a91..91a32f4441 100644 --- 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 index ec4d7296b1..6e6534a134 100644 --- 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 index 3bf7bda1f2..42856beaa7 100644 --- 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
Imports ```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 index 50486452c7..360a331b17 100644 --- 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 index f1fe91c9f6..d0fcdcfb9a 100644 --- 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 index 4d21a74f8c..cd2e5b299c 100644 --- a/src/foundation/fibered-equivalences.lagda.md +++ b/src/foundation/fibered-equivalences.lagda.md @@ -7,7 +7,6 @@ module foundation.fibered-equivalences where
Imports ```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 index 5d4ce207f6..52d6c85c57 100644 --- 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 index 3b0e0e540c..3702d997f1 100644 --- 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 index 86ec3c6427..09188bc215 100644 --- 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 ```
diff --git a/src/foundation/images.lagda.md b/src/foundation/images.lagda.md index 940bb4a10a..03a5373540 100644 --- 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 index d4f405c17e..c0cd11e783 100644 --- 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 index f0218d5e58..29e8d7b87a 100644 --- 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 ```
diff --git a/src/foundation/symmetric-cores-binary-relations.lagda.md b/src/foundation/symmetric-cores-binary-relations.lagda.md index d66db85e42..5bf1eea410 100644 --- 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
Imports ```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 ```
diff --git a/src/group-theory/centralizer-subgroups.lagda.md b/src/group-theory/centralizer-subgroups.lagda.md index d0b3d35b47..9d746c441b 100644 --- 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 index 5cf23f6b63..2c18d88dcd 100644 --- 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 ```
diff --git a/src/group-theory/cyclic-groups.lagda.md b/src/group-theory/cyclic-groups.lagda.md index 311b0caf6f..18d82a0b7a 100644 --- a/src/group-theory/cyclic-groups.lagda.md +++ b/src/group-theory/cyclic-groups.lagda.md @@ -8,7 +8,6 @@ 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 @@ -16,18 +15,11 @@ 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 ``` diff --git a/src/group-theory/generating-elements-groups.lagda.md b/src/group-theory/generating-elements-groups.lagda.md index 939899d394..f7ca727f75 100644 --- 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 index a6bba4f237..594ee4ee44 100644 --- 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 ``` diff --git a/src/order-theory/closure-operators-large-locales.lagda.md b/src/order-theory/closure-operators-large-locales.lagda.md index eab913d366..0222035bfd 100644 --- 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 index 4239522def..986129922c 100644 --- 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
Imports ```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 index 11a4775f2a..b19cfc8276 100644 --- 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
Imports ```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 index aa9e5d01b5..93e3fad22a 100644 --- 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
Imports ```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 index 84322ba57f..b83f3a51ad 100644 --- 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
Imports ```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 index aa8f7a8700..c7a2f64ebe 100644 --- 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
Imports ```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 index df8b43e316..554d772c09 100644 --- 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
Imports ```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 index 7cbfd34d86..0c05cbae6b 100644 --- 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
Imports ```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 index 4d8caa5c83..ed47826fb0 100644 --- a/src/order-theory/large-frames.lagda.md +++ b/src/order-theory/large-frames.lagda.md @@ -7,15 +7,12 @@ module order-theory.large-frames where
Imports ```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 @@ -23,7 +20,6 @@ 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 index 5e4c83ee33..30dd43ed3b 100644 --- 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
Imports ```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-meet-semilattices.lagda.md b/src/order-theory/large-meet-semilattices.lagda.md index 5faa1547fd..d0b50ba6be 100644 --- a/src/order-theory/large-meet-semilattices.lagda.md +++ b/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 diff --git a/src/order-theory/large-meet-subsemilattices.lagda.md b/src/order-theory/large-meet-subsemilattices.lagda.md index 38b7393131..efbdc78503 100644 --- a/src/order-theory/large-meet-subsemilattices.lagda.md +++ b/src/order-theory/large-meet-subsemilattices.lagda.md @@ -7,11 +7,8 @@ module order-theory.large-meet-subsemilattices where
Imports ```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.universe-levels open import order-theory.greatest-lower-bounds-large-posets diff --git a/src/order-theory/large-posets.lagda.md b/src/order-theory/large-posets.lagda.md index fb31b3ff9c..1c85ff51d6 100644 --- a/src/order-theory/large-posets.lagda.md +++ b/src/order-theory/large-posets.lagda.md @@ -7,16 +7,12 @@ module order-theory.large-posets where
Imports ```agda -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 -open import foundation.binary-relations open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.function-types open import foundation.identity-types open import foundation.large-binary-relations open import foundation.propositions diff --git a/src/order-theory/large-preorders.lagda.md b/src/order-theory/large-preorders.lagda.md index cc0f69e0bd..8044a4039b 100644 --- a/src/order-theory/large-preorders.lagda.md +++ b/src/order-theory/large-preorders.lagda.md @@ -9,9 +9,7 @@ module order-theory.large-preorders where ```agda open import category-theory.large-precategories -open import foundation.binary-relations open import foundation.dependent-pair-types -open import foundation.function-types open import foundation.identity-types open import foundation.large-binary-relations open import foundation.propositions diff --git a/src/order-theory/large-quotient-locales.lagda.md b/src/order-theory/large-quotient-locales.lagda.md index c3350b260f..7623efa54a 100644 --- a/src/order-theory/large-quotient-locales.lagda.md +++ b/src/order-theory/large-quotient-locales.lagda.md @@ -7,10 +7,8 @@ module order-theory.large-quotient-locales where
Imports ```agda -open import foundation.binary-relations open import foundation.identity-types open import foundation.large-binary-relations -open import foundation.propositions open import foundation.universe-levels open import order-theory.greatest-lower-bounds-large-posets diff --git a/src/order-theory/large-subframes.lagda.md b/src/order-theory/large-subframes.lagda.md index 961dbd2314..e71cd3fd20 100644 --- a/src/order-theory/large-subframes.lagda.md +++ b/src/order-theory/large-subframes.lagda.md @@ -7,12 +7,10 @@ module order-theory.large-subframes where
Imports ```agda -open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.function-types open import foundation.identity-types open import foundation.large-binary-relations -open import foundation.propositions open import foundation.subtypes open import foundation.universe-levels diff --git a/src/order-theory/large-subposets.lagda.md b/src/order-theory/large-subposets.lagda.md index dbc27c5689..45742cf499 100644 --- a/src/order-theory/large-subposets.lagda.md +++ b/src/order-theory/large-subposets.lagda.md @@ -7,11 +7,8 @@ module order-theory.large-subposets where
Imports ```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.subtypes open import foundation.universe-levels diff --git a/src/order-theory/large-subpreorders.lagda.md b/src/order-theory/large-subpreorders.lagda.md index 18448bf5a4..85e83e7c7e 100644 --- a/src/order-theory/large-subpreorders.lagda.md +++ b/src/order-theory/large-subpreorders.lagda.md @@ -7,7 +7,6 @@ module order-theory.large-subpreorders where
Imports ```agda -open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.large-binary-relations open import foundation.propositions diff --git a/src/order-theory/large-subsuplattices.lagda.md b/src/order-theory/large-subsuplattices.lagda.md index afa12fc71e..aa1996cd6e 100644 --- a/src/order-theory/large-subsuplattices.lagda.md +++ b/src/order-theory/large-subsuplattices.lagda.md @@ -7,10 +7,7 @@ module order-theory.large-subsuplattices where
Imports ```agda -open import foundation.binary-relations -open import foundation.identity-types open import foundation.large-binary-relations -open import foundation.propositions open import foundation.universe-levels open import order-theory.large-posets diff --git a/src/order-theory/lattices.lagda.md b/src/order-theory/lattices.lagda.md index 1f52d02c62..7dfeb5bad3 100644 --- a/src/order-theory/lattices.lagda.md +++ b/src/order-theory/lattices.lagda.md @@ -9,7 +9,6 @@ module order-theory.lattices where ```agda open import foundation.binary-relations open import foundation.dependent-pair-types -open import foundation.identity-types open import foundation.propositions open import foundation.sets open import foundation.universe-levels diff --git a/src/order-theory/meet-suplattices.lagda.md b/src/order-theory/meet-suplattices.lagda.md index ec3d39d588..c9ee77f4e0 100644 --- a/src/order-theory/meet-suplattices.lagda.md +++ b/src/order-theory/meet-suplattices.lagda.md @@ -9,7 +9,6 @@ module order-theory.meet-suplattices where ```agda open import foundation.binary-relations open import foundation.dependent-pair-types -open import foundation.identity-types open import foundation.propositions open import foundation.sets open import foundation.universe-levels diff --git a/src/order-theory/nuclei-large-locales.lagda.md b/src/order-theory/nuclei-large-locales.lagda.md index ed885d3815..ec560b5282 100644 --- a/src/order-theory/nuclei-large-locales.lagda.md +++ b/src/order-theory/nuclei-large-locales.lagda.md @@ -8,7 +8,6 @@ module order-theory.nuclei-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/powers-of-large-locales.lagda.md b/src/order-theory/powers-of-large-locales.lagda.md index dc2912e011..8f06828c26 100644 --- a/src/order-theory/powers-of-large-locales.lagda.md +++ b/src/order-theory/powers-of-large-locales.lagda.md @@ -7,10 +7,8 @@ module order-theory.powers-of-large-locales where
Imports ```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/suplattices.lagda.md b/src/order-theory/suplattices.lagda.md index 5b9e36c71f..23b0a56327 100644 --- a/src/order-theory/suplattices.lagda.md +++ b/src/order-theory/suplattices.lagda.md @@ -9,7 +9,6 @@ module order-theory.suplattices where ```agda open import foundation.binary-relations open import foundation.dependent-pair-types -open import foundation.identity-types open import foundation.propositions open import foundation.sets open import foundation.universe-levels diff --git a/src/orthogonal-factorization-systems/closed-modalities.lagda.md b/src/orthogonal-factorization-systems/closed-modalities.lagda.md index 2ab456ac35..9084061785 100644 --- a/src/orthogonal-factorization-systems/closed-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/closed-modalities.lagda.md @@ -15,7 +15,6 @@ open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.propositions -open import foundation.subuniverses open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels diff --git a/src/orthogonal-factorization-systems/locally-small-modal-operators.lagda.md b/src/orthogonal-factorization-systems/locally-small-modal-operators.lagda.md index b45cb0a92a..88185472d4 100644 --- a/src/orthogonal-factorization-systems/locally-small-modal-operators.lagda.md +++ b/src/orthogonal-factorization-systems/locally-small-modal-operators.lagda.md @@ -8,13 +8,7 @@ module orthogonal-factorization-systems.locally-small-modal-operators where ```agda open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.function-types open import foundation.locally-small-types -open import foundation.propositions -open import foundation.sigma-closed-subuniverses -open import foundation.small-types -open import foundation.subuniverses open import foundation.universe-levels open import orthogonal-factorization-systems.modal-operators diff --git a/src/orthogonal-factorization-systems/modal-operators.lagda.md b/src/orthogonal-factorization-systems/modal-operators.lagda.md index 024a6cfd35..ea6b4b64dc 100644 --- a/src/orthogonal-factorization-systems/modal-operators.lagda.md +++ b/src/orthogonal-factorization-systems/modal-operators.lagda.md @@ -10,9 +10,7 @@ module orthogonal-factorization-systems.modal-operators where open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types -open import foundation.locally-small-types open import foundation.propositions -open import foundation.sigma-closed-subuniverses open import foundation.small-types open import foundation.subuniverses open import foundation.universe-levels diff --git a/src/orthogonal-factorization-systems/reflective-modalities.lagda.md b/src/orthogonal-factorization-systems/reflective-modalities.lagda.md index 732bbddcde..c071673c5f 100644 --- a/src/orthogonal-factorization-systems/reflective-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/reflective-modalities.lagda.md @@ -7,12 +7,9 @@ module orthogonal-factorization-systems.reflective-modalities where
Imports ```agda -open import foundation.cartesian-product-types open import foundation.dependent-pair-types -open import foundation.propositions open import foundation.universe-levels -open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.reflective-subuniverses ``` diff --git a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md index d68ad0d31a..b7fb9d002b 100644 --- a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md @@ -9,7 +9,6 @@ module orthogonal-factorization-systems.reflective-subuniverses where ```agda open import foundation.cartesian-product-types open import foundation.dependent-pair-types -open import foundation.function-types open import foundation.propositions open import foundation.subuniverses open import foundation.universe-levels diff --git a/src/orthogonal-factorization-systems/sigma-closed-modalities.lagda.md b/src/orthogonal-factorization-systems/sigma-closed-modalities.lagda.md index a180b3b3b0..efb9bfd560 100644 --- a/src/orthogonal-factorization-systems/sigma-closed-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/sigma-closed-modalities.lagda.md @@ -9,12 +9,10 @@ module orthogonal-factorization-systems.sigma-closed-modalities where ```agda open import foundation.dependent-pair-types open import foundation.function-types -open import foundation.propositions open import foundation.sigma-closed-subuniverses open import foundation.universe-levels open import orthogonal-factorization-systems.modal-operators -open import orthogonal-factorization-systems.reflective-subuniverses ```
diff --git a/src/orthogonal-factorization-systems/sigma-closed-reflective-modalities.lagda.md b/src/orthogonal-factorization-systems/sigma-closed-reflective-modalities.lagda.md index e51f717291..4abbb4bf5d 100644 --- a/src/orthogonal-factorization-systems/sigma-closed-reflective-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/sigma-closed-reflective-modalities.lagda.md @@ -9,14 +9,10 @@ module orthogonal-factorization-systems.sigma-closed-reflective-modalities where ```agda open import foundation.cartesian-product-types open import foundation.dependent-pair-types -open import foundation.function-types -open import foundation.propositions -open import foundation.sigma-closed-subuniverses open import foundation.universe-levels open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.reflective-modalities -open import orthogonal-factorization-systems.reflective-subuniverses open import orthogonal-factorization-systems.sigma-closed-modalities ``` diff --git a/src/orthogonal-factorization-systems/sigma-closed-reflective-subuniverses.lagda.md b/src/orthogonal-factorization-systems/sigma-closed-reflective-subuniverses.lagda.md index 0aa0fb60f1..5b037b7ed8 100644 --- a/src/orthogonal-factorization-systems/sigma-closed-reflective-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/sigma-closed-reflective-subuniverses.lagda.md @@ -8,12 +8,9 @@ module orthogonal-factorization-systems.sigma-closed-reflective-subuniverses whe ```agda open import foundation.dependent-pair-types -open import foundation.function-types -open import foundation.propositions open import foundation.sigma-closed-subuniverses open import foundation.universe-levels -open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.reflective-subuniverses ``` diff --git a/src/structured-types/dependent-products-pointed-types.lagda.md b/src/structured-types/dependent-products-pointed-types.lagda.md index 919359ada8..a381e35e41 100644 --- a/src/structured-types/dependent-products-pointed-types.lagda.md +++ b/src/structured-types/dependent-products-pointed-types.lagda.md @@ -7,11 +7,7 @@ module structured-types.dependent-products-pointed-types where
Imports ```agda -open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types -open import foundation.function-extensionality -open import foundation.identity-types -open import foundation.unital-binary-operations open import foundation.universe-levels open import structured-types.pointed-types diff --git a/src/structured-types/dependent-products-wild-monoids.lagda.md b/src/structured-types/dependent-products-wild-monoids.lagda.md index c46c1e9827..183ccb58a5 100644 --- a/src/structured-types/dependent-products-wild-monoids.lagda.md +++ b/src/structured-types/dependent-products-wild-monoids.lagda.md @@ -11,9 +11,7 @@ open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.homotopies -open import foundation.homotopy-induction open import foundation.identity-types -open import foundation.sets open import foundation.unit-type open import foundation.universe-levels diff --git a/src/structured-types/function-h-spaces.lagda.md b/src/structured-types/function-h-spaces.lagda.md index 4a0f113953..05b8a63e3c 100644 --- a/src/structured-types/function-h-spaces.lagda.md +++ b/src/structured-types/function-h-spaces.lagda.md @@ -7,9 +7,6 @@ module structured-types.function-h-spaces where
Imports ```agda -open import foundation.action-on-identifications-functions -open import foundation.dependent-pair-types -open import foundation.function-extensionality open import foundation.identity-types open import foundation.unital-binary-operations open import foundation.universe-levels diff --git a/src/structured-types/function-wild-monoids.lagda.md b/src/structured-types/function-wild-monoids.lagda.md index 487efefb05..154a0e8116 100644 --- a/src/structured-types/function-wild-monoids.lagda.md +++ b/src/structured-types/function-wild-monoids.lagda.md @@ -7,17 +7,9 @@ module structured-types.function-wild-monoids where
Imports ```agda -open import foundation.action-on-identifications-functions -open import foundation.dependent-pair-types -open import foundation.function-extensionality -open import foundation.homotopies -open import foundation.homotopy-induction open import foundation.identity-types -open import foundation.sets -open import foundation.unit-type open import foundation.universe-levels -open import structured-types.dependent-products-h-spaces open import structured-types.dependent-products-wild-monoids open import structured-types.h-spaces open import structured-types.pointed-types diff --git a/src/structured-types/h-spaces.lagda.md b/src/structured-types/h-spaces.lagda.md index d321ba613f..a15b9a8bb3 100644 --- a/src/structured-types/h-spaces.lagda.md +++ b/src/structured-types/h-spaces.lagda.md @@ -20,7 +20,6 @@ open import foundation.unital-binary-operations open import foundation.universe-levels open import foundation-core.endomorphisms -open import foundation-core.propositions open import structured-types.magmas open import structured-types.noncoherent-h-spaces diff --git a/src/structured-types/morphisms-wild-monoids.lagda.md b/src/structured-types/morphisms-wild-monoids.lagda.md index 0e86a382d8..d18b3912a9 100644 --- a/src/structured-types/morphisms-wild-monoids.lagda.md +++ b/src/structured-types/morphisms-wild-monoids.lagda.md @@ -7,23 +7,12 @@ module structured-types.morphisms-wild-monoids where
Imports ```agda -open import foundation.action-on-identifications-functions -open import foundation.contractible-types open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.fundamental-theorem-of-identity-types -open import foundation.homotopies open import foundation.identity-types -open import foundation.propositions -open import foundation.sets -open import foundation.subtype-identity-principle -open import foundation.subtypes open import foundation.universe-levels open import group-theory.homomorphisms-semigroups -open import group-theory.monoids -open import structured-types.h-spaces open import structured-types.morphisms-h-spaces open import structured-types.pointed-maps open import structured-types.wild-monoids diff --git a/src/structured-types/wild-monoids.lagda.md b/src/structured-types/wild-monoids.lagda.md index 6c4461e79f..e1c64a886f 100644 --- a/src/structured-types/wild-monoids.lagda.md +++ b/src/structured-types/wild-monoids.lagda.md @@ -10,13 +10,10 @@ module structured-types.wild-monoids where open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.identity-types -open import foundation.propositions open import foundation.unit-type open import foundation.universe-levels open import structured-types.h-spaces -open import structured-types.morphisms-h-spaces -open import structured-types.pointed-maps open import structured-types.pointed-types ``` diff --git a/src/synthetic-homotopy-theory/conjugation-loops.lagda.md b/src/synthetic-homotopy-theory/conjugation-loops.lagda.md index 9e6d4594fe..f904e324d8 100644 --- a/src/synthetic-homotopy-theory/conjugation-loops.lagda.md +++ b/src/synthetic-homotopy-theory/conjugation-loops.lagda.md @@ -8,7 +8,6 @@ module synthetic-homotopy-theory.conjugation-loops where ```agda open import foundation.dependent-pair-types -open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.universe-levels diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md index 0c7235224f..f6ef8f235a 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md @@ -7,11 +7,8 @@ module synthetic-homotopy-theory.flattening-lemma-pushouts where
Imports ```agda -open import foundation.action-on-identifications-dependent-functions -open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-maps open import foundation.commuting-triangles-of-maps -open import foundation.dependent-identifications open import foundation.dependent-pair-types open import foundation.equality-dependent-pair-types open import foundation.equivalences diff --git a/src/trees/fibers-directed-trees.lagda.md b/src/trees/fibers-directed-trees.lagda.md index 9f4576c746..b1cff222b1 100644 --- a/src/trees/fibers-directed-trees.lagda.md +++ b/src/trees/fibers-directed-trees.lagda.md @@ -7,21 +7,15 @@ module trees.fibers-directed-trees where
Imports ```agda -open import foundation.contractible-types open import foundation.coproduct-types open import foundation.dependent-pair-types -open import foundation.equality-dependent-pair-types open import foundation.equivalences -open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types -open import foundation.raising-universe-levels -open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import graph-theory.directed-graphs open import graph-theory.fibers-directed-graphs -open import graph-theory.walks-directed-graphs open import trees.bases-directed-trees open import trees.directed-trees diff --git a/src/univalent-combinatorics/universal-property-standard-finite-types.lagda.md b/src/univalent-combinatorics/universal-property-standard-finite-types.lagda.md index 3d655eb3b9..2126d8134a 100644 --- a/src/univalent-combinatorics/universal-property-standard-finite-types.lagda.md +++ b/src/univalent-combinatorics/universal-property-standard-finite-types.lagda.md @@ -13,7 +13,6 @@ open import foundation.cartesian-product-types open import foundation.contractible-types open import foundation.coproduct-types open import foundation.dependent-pair-types -open import foundation.equality-cartesian-product-types open import foundation.equivalences open import foundation.function-extensionality open import foundation.function-types