Remove empty foundation modules and replace them by their core coun…

…terparts (#644)

There were 21 completely empty `foundation` files that are removed by
this PR and replaced by their core counterparts. There are still 14
empty modules outside of `foundation`, some with commented code.

FILE-CONVENTIONS.md

@@ -35,27 +35,42 @@ Every file should begin with a header in the following format:
 # The title of the file
 ```
 
-and immediately after this, any option pragmas, then the module declaration then
-public imports, if any, should be declared. E.g.
+Directly after the header, include an Agda code block containing
+
+- any option pragmas,
+- the main module declaration,
+- any public import statements
+
+in this order. E.g.
 
 ````md
 ```agda
-{-# OPTIONS --safe #-}
+{-# OPTIONS ... #-}
 
-module foundation.dependent-pair-types where
+module ... where
 
-open import foundation-core.dependent-pair-types public
+open import ... public
 ```
 ````
 
 ### Imports block
 
-After the module declaration, include an Agda code block of all module imports
-starting with `<details><summary>Imports</summary>` and ending with
-`</details>`. This Agda block should only contain module imports. Do not import
-further modules later in the file. On the documentation pages, this Agda imports
-block will be hidden by default, but it can be revealed by clicking on the
-_Imports_ link.
+After the module declaration, include an Agda code block of all non-public
+module imports starting with `<details><summary>Imports</summary>` and ending
+with `</details>`. This block should only contain module imports and there
+should have no further import statements after it. In the rendered markdown, the
+contents of this block will be hidden by default, but can be revealed by
+clicking on _Imports_.
+
+````md
+<details><summary>Imports</summary>
+
+```agda
+open import ...
+```
+
+</details>
+````
 
 ### Sections and headings
 
@@ -65,10 +80,10 @@ subsubsections. Use `##` headings for the main sections of the file and reserve
 `## Definitions`, and `## Properties`. Occasionally, you might include a section
 like `## Examples` or `## Theorem`, based on the purpose of the file.
 
-Ideally, the first section of a file explains the idea, the second section
-proceeds to give the main definition that is the focus of the file, then the
-third section proceeds possibly with examples or by deriving basic properties of
-the defined concept.
+Ideally, depending on the purpose of the file, the first section explains the
+main idea, the second section proceeds to give the main definition that is the
+focus of the file, then the third section proceeds possibly with examples or by
+deriving basic properties of the defined concept.
 
 #### Subsections
 
@@ -105,6 +120,6 @@ contents of the file.
 - An instructive example of a file with the expected structure is
   [`foundation.cantor-schroder-bernstein-escardo`](https://raw.githubusercontent.com/UniMath/agda-unimath/master/src/foundation/cantor-schroder-bernstein-escardo.lagda.md).
 
-Please note that some conventions above are enforced by our `pre-commit` hooks.
-You can read more about them in our
+Please note that some of the conventions above are enforced by our `pre-commit`
+hooks. You can read more about them in our
 [installation guide](HOWTO-INSTALL.md#pre-commit-hooks).

src/elementary-number-theory/powers-of-two.lagda.md

@@ -16,16 +16,16 @@ open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.parity-natural-numbers
 open import elementary-number-theory.strong-induction-natural-numbers
 
+open import foundation.dependent-pair-types
+open import foundation.equality-cartesian-product-types
+open import foundation.functions
 open import foundation.split-surjective-maps
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
 open import foundation-core.coproduct-types
-open import foundation-core.dependent-pair-types
 open import foundation-core.empty-types
-open import foundation-core.equality-cartesian-product-types
 open import foundation-core.equivalences
-open import foundation-core.functions
 open import foundation-core.identity-types
 open import foundation-core.injective-maps
 ```

src/elementary-number-theory/type-arithmetic-natural-numbers.lagda.md

@@ -15,6 +15,8 @@ open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.parity-natural-numbers
 open import elementary-number-theory.powers-of-two
 
+open import foundation.dependent-pair-types
+open import foundation.functions
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-coproduct-types
 open import foundation.iterating-functions
@@ -26,10 +28,8 @@ open import foundation.unit-type
 
 open import foundation-core.cartesian-product-types
 open import foundation-core.coproduct-types
-open import foundation-core.dependent-pair-types
 open import foundation-core.empty-types
 open import foundation-core.equivalences
-open import foundation-core.functions
 open import foundation-core.identity-types
 open import foundation-core.injective-maps
 open import foundation-core.negation

src/foundation-core.lagda.md

@@ -5,52 +5,36 @@
 ```agda
 module foundation-core where
 
-open import foundation-core.0-maps public
 open import foundation-core.1-types public
-open import foundation-core.automorphisms public
 open import foundation-core.cartesian-product-types public
 open import foundation-core.coherently-invertible-maps public
-open import foundation-core.commuting-3-simplices-of-homotopies public
-open import foundation-core.commuting-3-simplices-of-maps public
 open import foundation-core.commuting-cubes-of-maps public
 open import foundation-core.commuting-squares-of-maps public
-open import foundation-core.commuting-triangles-of-homotopies public
 open import foundation-core.commuting-triangles-of-maps public
-open import foundation-core.cones-over-cospans public
 open import foundation-core.constant-maps public
 open import foundation-core.contractible-maps public
 open import foundation-core.contractible-types public
 open import foundation-core.coproduct-types public
-open import foundation-core.cospans public
 open import foundation-core.decidable-propositions public
-open import foundation-core.dependent-pair-types public
 open import foundation-core.diagonal-maps-of-types public
 open import foundation-core.discrete-types public
 open import foundation-core.embeddings public
 open import foundation-core.empty-types public
 open import foundation-core.endomorphisms public
-open import foundation-core.equality-cartesian-product-types public
 open import foundation-core.equality-dependent-pair-types public
-open import foundation-core.equality-fibers-of-maps public
 open import foundation-core.equivalence-induction public
 open import foundation-core.equivalence-relations public
 open import foundation-core.equivalences public
-open import foundation-core.faithful-maps public
 open import foundation-core.fibers-of-maps public
 open import foundation-core.function-extensionality public
-open import foundation-core.functions public
 open import foundation-core.functoriality-dependent-function-types public
 open import foundation-core.functoriality-dependent-pair-types public
-open import foundation-core.functoriality-fibers-of-maps public
 open import foundation-core.functoriality-function-types public
-open import foundation-core.fundamental-theorem-of-identity-types public
 open import foundation-core.homotopies public
-open import foundation-core.identity-systems public
 open import foundation-core.identity-types public
 open import foundation-core.injective-maps public
 open import foundation-core.involutions public
 open import foundation-core.logical-equivalences public
-open import foundation-core.morphisms-cospans public
 open import foundation-core.negation public
 open import foundation-core.path-split-maps public
 open import foundation-core.propositional-maps public
@@ -61,15 +45,11 @@ open import foundation-core.sections public
 open import foundation-core.sets public
 open import foundation-core.singleton-induction public
 open import foundation-core.small-types public
-open import foundation-core.subtype-identity-principle public
 open import foundation-core.subtypes public
 open import foundation-core.truncated-maps public
 open import foundation-core.truncated-types public
 open import foundation-core.truncation-levels public
-open import foundation-core.type-arithmetic-cartesian-product-types public
-open import foundation-core.type-arithmetic-dependent-pair-types public
 open import foundation-core.univalence public
 open import foundation-core.universal-property-pullbacks public
 open import foundation-core.universal-property-truncation public
-open import foundation-core.universe-levels public
 ```

src/foundation-core/1-types.lagda.md

@@ -7,13 +7,14 @@ module foundation-core.1-types where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation-core.dependent-pair-types
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
 open import foundation-core.equivalences
 open import foundation-core.identity-types
 open import foundation-core.sets
 open import foundation-core.truncated-types
 open import foundation-core.truncation-levels
-open import foundation-core.universe-levels
 ```
 
 </details>