cleaning up transport and dependent identifications files (#650)

- correcting typos in the tables of files related to identity types
- Moving facts about transport from `foundation.identity-types` to
`foundation.transport`
- Renaming dependent paths to dependent identifications
- Renaming path-overs to dependent identifications
- Factoring out the computations of transport to their specific files,
eg transport in cartesian products to cartesian products, transport in
identity types to identity types, and so on.
- Moving `functions` to `function-types` to more clearly support both
operations on function types as well as other lemmas about function
types.
- Cleaning up dependent identifications file. There is still some
conceptual work to be done here. Refactoring this is highly nontrivial.

src/category-theory/functors-large-precategories.lagda.md

@@ -10,7 +10,7 @@ module category-theory.functors-large-precategories where
 open import category-theory.large-precategories
 
 open import foundation.action-on-identifications-functions
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.universe-levels
 ```

src/category-theory/functors-precategories.lagda.md

@@ -12,7 +12,7 @@ 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.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.universe-levels

src/category-theory/groupoids.lagda.md

@@ -18,7 +18,7 @@ open import foundation.1-types
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
-open import foundation.functions
+open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types

src/category-theory/isomorphisms-precategories.lagda.md

@@ -13,7 +13,7 @@ open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
-open import foundation.functions
+open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions

src/category-theory/natural-isomorphisms-precategories.lagda.md

@@ -13,7 +13,7 @@ open import category-theory.natural-transformations-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.propositions
 open import foundation.universe-levels
 ```

src/category-theory/natural-transformations-precategories.lagda.md

@@ -14,7 +14,7 @@ open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.function-extensionality
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.propositions

src/category-theory/precategories.lagda.md

@@ -10,7 +10,7 @@ module category-theory.precategories where
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets

src/category-theory/slice-precategories.lagda.md

@@ -18,7 +18,7 @@ open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.equality-dependent-pair-types
 open import foundation.equivalences
-open import foundation.functions
+open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
 open import foundation.identity-types

src/commutative-algebra/joins-radical-ideals-commutative-rings.lagda.md

@@ -20,7 +20,7 @@ open import commutative-algebra.radicals-of-ideals-commutative-rings
 open import commutative-algebra.subsets-commutative-rings
 
 open import foundation.dependent-pair-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.universe-levels
 

src/commutative-algebra/poset-of-radical-ideals-commutative-rings.lagda.md

@@ -11,7 +11,7 @@ open import commutative-algebra.commutative-rings
 open import commutative-algebra.poset-of-ideals-commutative-rings
 open import commutative-algebra.radical-ideals-commutative-rings
 
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.subtypes

src/commutative-algebra/prime-ideals-commutative-rings.lagda.md

@@ -18,7 +18,7 @@ open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.disjunction
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.universe-levels

src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md

@@ -22,7 +22,7 @@ open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.existential-quantification
-open import foundation.functions
+open import foundation.function-types
 open import foundation.logical-equivalences
 open import foundation.propositional-truncations
 open import foundation.propositions

src/commutative-algebra/sums-commutative-rings.lagda.md

@@ -14,7 +14,7 @@ open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.unit-type

src/commutative-algebra/sums-commutative-semirings.lagda.md

@@ -12,7 +12,7 @@ open import commutative-algebra.commutative-semirings
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.natural-numbers
 
-open import foundation.functions
+open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.universe-levels

src/elementary-number-theory/absolute-value-integers.lagda.md

@@ -17,7 +17,7 @@ open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.unit-type
 ```

src/elementary-number-theory/addition-integers.lagda.md

@@ -19,7 +19,7 @@ open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equivalences
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.interchange-law

src/elementary-number-theory/addition-natural-numbers.lagda.md

@@ -15,7 +15,7 @@ open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.empty-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.interchange-law

src/elementary-number-theory/based-induction-natural-numbers.lagda.md

@@ -10,7 +10,7 @@ module elementary-number-theory.based-induction-natural-numbers where
 open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.natural-numbers
 
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.universe-levels
 ```

src/elementary-number-theory/based-strong-induction-natural-numbers.lagda.md

@@ -17,7 +17,7 @@ open import foundation.contractible-types
 open import foundation.coproduct-types
 open import foundation.empty-types
 open import foundation.function-extensionality
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.universe-levels

src/elementary-number-theory/bezouts-lemma-integers.lagda.md

@@ -26,7 +26,7 @@ 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.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.transport
 open import foundation.unit-type

src/elementary-number-theory/bounded-sums-arithmetic-functions.lagda.md

@@ -14,7 +14,7 @@ open import elementary-number-theory.nonzero-natural-numbers
 open import foundation.coproduct-types
 open import foundation.decidable-propositions
 open import foundation.decidable-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.universe-levels
 
 open import ring-theory.rings

src/elementary-number-theory/congruence-integers.lagda.md

@@ -18,7 +18,7 @@ open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.transport
 open import foundation.universe-levels

src/elementary-number-theory/decidable-types.lagda.md

@@ -17,7 +17,7 @@ open import foundation.coproduct-types
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.unit-type
 open import foundation.universe-levels
 ```

src/elementary-number-theory/distance-natural-numbers.lagda.md

@@ -17,7 +17,7 @@ open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.transport
 open import foundation.unit-type

src/elementary-number-theory/divisibility-integers.lagda.md

@@ -21,7 +21,7 @@ open import foundation.coproduct-types
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.negation
 open import foundation.propositional-maps

src/elementary-number-theory/equality-integers.lagda.md

@@ -21,7 +21,7 @@ open import foundation.discrete-types
 open import foundation.empty-types
 open import foundation.equality-dependent-pair-types
 open import foundation.equivalences
-open import foundation.functions
+open import foundation.function-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
 open import foundation.propositions

src/elementary-number-theory/equality-natural-numbers.lagda.md

@@ -16,7 +16,7 @@ open import foundation.decidable-equality
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
-open import foundation.functions
+open import foundation.function-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
 open import foundation.set-truncations

src/elementary-number-theory/finitary-natural-numbers.lagda.md

@@ -18,7 +18,7 @@ open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.universe-levels

src/elementary-number-theory/finitely-cyclic-maps.lagda.md

@@ -13,7 +13,7 @@ open import elementary-number-theory.natural-numbers
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equivalences
-open import foundation.functions
+open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.iterating-functions

src/elementary-number-theory/greatest-common-divisor-integers.lagda.md

@@ -20,7 +20,7 @@ open import foundation.cartesian-product-types
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.identity-types
 open import foundation.logical-equivalences

src/elementary-number-theory/inequality-integers.lagda.md

@@ -15,7 +15,7 @@ open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.functoriality-coproduct-types
 open import foundation.identity-types
 open import foundation.propositions

src/elementary-number-theory/inequality-natural-numbers.lagda.md

@@ -17,7 +17,7 @@ open import foundation.coproduct-types
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.functoriality-coproduct-types
 open import foundation.identity-types
 open import foundation.negation

src/elementary-number-theory/initial-segments-natural-numbers.lagda.md

@@ -11,7 +11,7 @@ open import elementary-number-theory.maximum-natural-numbers
 open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.subtypes

src/elementary-number-theory/integers.lagda.md

@@ -16,7 +16,7 @@ open import foundation.embeddings
 open import foundation.empty-types
 open import foundation.equality-coproduct-types
 open import foundation.equivalences
-open import foundation.functions
+open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.injective-maps

src/elementary-number-theory/modular-arithmetic-standard-finite-types.lagda.md

@@ -23,7 +23,7 @@ open import foundation.decidable-propositions
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.split-surjective-maps

src/elementary-number-theory/modular-arithmetic.lagda.md

@@ -29,7 +29,7 @@ open import foundation.dependent-pair-types
 open import foundation.discrete-types
 open import foundation.empty-types
 open import foundation.equivalences
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.negation

src/elementary-number-theory/multiplication-integers.lagda.md

@@ -21,7 +21,7 @@ open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types
 open import foundation.embeddings
 open import foundation.empty-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.interchange-law

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

@@ -11,7 +11,7 @@ open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.equivalences
-open import foundation.functions
+open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.injective-maps

src/elementary-number-theory/parity-natural-numbers.lagda.md

@@ -16,7 +16,7 @@ open import foundation.action-on-identifications-functions
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.negation
 open import foundation.universe-levels

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

@@ -19,7 +19,7 @@ open import elementary-number-theory.strong-induction-natural-numbers
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.split-surjective-maps
 open import foundation.transport
 open import foundation.universe-levels

src/elementary-number-theory/sieve-of-eratosthenes.lagda.md

@@ -22,7 +22,7 @@ open import foundation.coproduct-types
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.unit-type
 open import foundation.universe-levels

src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md

@@ -17,7 +17,7 @@ open import foundation.coproduct-types
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.functoriality-coproduct-types
 open import foundation.identity-types
 open import foundation.negation

src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md

@@ -13,7 +13,7 @@ open import elementary-number-theory.strict-inequality-natural-numbers
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.empty-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
 open import foundation.negation

src/elementary-number-theory/strong-induction-natural-numbers.lagda.md

@@ -16,7 +16,7 @@ open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.function-extensionality
-open import foundation.functions
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.universe-levels