Cleaning up some stuff in species (#575)

In this PR I am cleaning up some of the files in and related to the
theory of species.

- I have chosen some more natural file names
- English grammar corrected
- Highlighted defined terms in `## Idea` sections
- Fixed indentation levels: Sometimes 4 space increments are used,
instead of the standard 2 space increments.
- Sometimes an entire definition was wrapped in parentheses for no
reason. I removed those parentheses.
- Refactored some constructions of equivalences: Often they are
constructed in one go, even if the construction naturally factors
through the construction of the underlying map, its inverse, and
homotopies proving that the inverse is a section and a retraction. If a
construction of an equivalence naturally factors through these steps, it
is better to turn these steps into separate definitions which can be
used later.
- Sometimes the fact that subuniverses are closed under equivalences was
reproven during a construction. There is a definition
`is-in-subuniverse-equiv` for this, so it is better and faster to use
it.
- The hypotheses on subuniverses were complicated expressions and were
repeated often. They warranted to be definitions, so I made those
definitions and factored out the complicated expressions.
- Anonymous modules should not cross over sections in a file.

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

@@ -8,6 +8,7 @@ module foundation-core.empty-types where
 
 ```agda
 open import foundation.propositions
+open import foundation.subuniverses
 
 open import foundation-core.dependent-pair-types
 open import foundation-core.embeddings
@@ -30,6 +31,8 @@ empty type.
 
 ## Definition
 
+### Empty types
+
 ```agda
 data empty : UU lzero where
 

src/foundation.lagda.md

@@ -223,7 +223,9 @@ open import foundation.standard-apartness-relations public
 open import foundation.strongly-extensional-maps public
 open import foundation.structure public
 open import foundation.structure-identity-principle public
+open import foundation.structured-type-duality public
 open import foundation.subterminal-types public
+open import foundation.subtype-duality public
 open import foundation.subtype-identity-principle public
 open import foundation.subtypes public
 open import foundation.subuniverses public

src/foundation/contractible-types.lagda.md

@@ -87,6 +87,34 @@ abstract
   is-contr-Contr l = pair (center-Contr l) contraction-Contr
 ```
 
+### The predicate that a subuniverse contains any contractible types
+
+```agda
+contains-contractible-types-subuniverse :
+  {l1 l2 : Level} → subuniverse l1 l2 → UU (lsuc l1 ⊔ l2)
+contains-contractible-types-subuniverse {l1} P =
+  (X : UU l1) → is-contr X → is-in-subuniverse P X
+```
+
+### The predicate that a subuniverse is closed under the `is-contr` predicate
+
+We state a general form involving two universes, and a more traditional form
+using a single universe
+
+```agda
+is-closed-under-is-contr-subuniverses :
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : subuniverse l1 l3) →
+  UU (lsuc l1 ⊔ l2 ⊔ l3)
+is-closed-under-is-contr-subuniverses P Q =
+  (X : type-subuniverse P) →
+  is-in-subuniverse Q (is-contr (inclusion-subuniverse P X))
+
+is-closed-under-is-contr-subuniverse :
+  {l1 l2 : Level} (P : subuniverse l1 l2) → UU (lsuc l1 ⊔ l2)
+is-closed-under-is-contr-subuniverse P =
+  is-closed-under-is-contr-subuniverses P P
+```
+
 ## Properties
 
 ### If two types are equivalent then so are the propositions that they are contractible