Refactor precomposition (#937)

This PR refactors precomposition, following difficulties that people
have been facing around where to put stuff involving precomposition, and
cyclic dependencies that are too easily arising. In fact, it was quite a
knot to untie. At the core of the knot was what is now called the
(dependent) universal property of equivalences, which is in its own
separate file now. I created tables, and did some minor code formatting,
but please note that this is not the main purpose of this PR.

Makefile

@@ -4,7 +4,7 @@
 # files, and if these options are pervasive (i.e. they need to be enabled in all
 # modules that include the modules that have them enabled), then they need to be
 # added to the everything file as well.
-everythingOpts := --guardedness  --cohesion --flat-split
+everythingOpts := --guardedness --cohesion --flat-split
 # use "$ export AGDAVERBOSE=-v20" if you want to see all
 AGDAVERBOSE ?= -v1
 AGDAFILES := $(shell find src -name temp -prune -o -type f \( -name "*.lagda.md" -not -name "everything.lagda.md" \) -print)

src/category-theory/dependent-products-of-large-categories.lagda.md

@@ -14,7 +14,6 @@ open import category-theory.large-precategories
 
 open import foundation.equivalences
 open import foundation.function-extensionality
-open import foundation.function-types
 open import foundation.functoriality-dependent-function-types
 open import foundation.identity-types
 open import foundation.sets

src/category-theory/epimorphisms-in-large-precategories.lagda.md

@@ -10,10 +10,8 @@ module category-theory.epimorphisms-in-large-precategories where
 open import category-theory.isomorphisms-in-large-precategories
 open import category-theory.large-precategories
 
-open import foundation.action-on-identifications-functions
 open import foundation.embeddings
 open import foundation.equivalences
-open import foundation.identity-types
 open import foundation.propositions
 open import foundation.universe-levels
 ```

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

@@ -10,8 +10,6 @@ module category-theory.functors-large-categories where
 open import category-theory.functors-large-precategories
 open import category-theory.large-categories
 
-open import foundation.action-on-identifications-functions
-open import foundation.function-types
 open import foundation.identity-types
 open import foundation.universe-levels
 ```
@@ -21,7 +19,7 @@ open import foundation.universe-levels
 ## Idea
 
 A **functor** from a [large category](category-theory.large-categories.md) `C`
-to a large category `D` is just a
+to a large category `D` is a
 [functor](category-theory.functors-large-precategories.md) between the
 underlying [large precategories](category-theory.large-precategories.md) of `C`
 and `D`. In other words, functors of large categories consist of:

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

@@ -10,20 +10,12 @@ module category-theory.functors-nonunital-precategories where
 open import category-theory.functors-set-magmoids
 open import category-theory.maps-set-magmoids
 open import category-theory.nonunital-precategories
-open import category-theory.set-magmoids
 
-open import foundation.action-on-identifications-functions
-open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
-open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
-open import foundation.iterated-dependent-product-types
-open import foundation.propositions
-open import foundation.subtypes
-open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
 ```
 

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

@@ -19,7 +19,6 @@ open import foundation.equivalences
 open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
-open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.subtypes
 open import foundation.type-arithmetic-dependent-pair-types

src/category-theory/gaunt-categories.lagda.md

@@ -19,7 +19,6 @@ open import category-theory.rigid-objects-categories
 open import category-theory.strict-categories
 
 open import foundation.cartesian-product-types
-open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions

src/category-theory/initial-objects-large-categories.lagda.md

@@ -10,7 +10,6 @@ module category-theory.initial-objects-large-categories where
 open import category-theory.initial-objects-large-precategories
 open import category-theory.large-categories
 
-open import foundation.contractible-types
 open import foundation.universe-levels
 ```
 

src/category-theory/isomorphism-induction-precategories.lagda.md

@@ -11,7 +11,6 @@ open import category-theory.isomorphisms-in-precategories
 open import category-theory.precategories
 
 open import foundation.commuting-triangles-of-maps
-open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.identity-systems

src/category-theory/large-subcategories.lagda.md

@@ -7,7 +7,6 @@ module category-theory.large-subcategories where
 <details><summary>Imports</summary>
 
 ```agda
-open import category-theory.isomorphisms-in-large-categories
 open import category-theory.large-categories
 open import category-theory.large-subprecategories
 

src/category-theory/maps-categories.lagda.md

@@ -10,8 +10,6 @@ module category-theory.maps-categories where
 open import category-theory.categories
 open import category-theory.maps-precategories
 
-open import foundation.contractible-types
-open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.homotopies
 open import foundation.identity-types

src/category-theory/maps-from-small-to-large-precategories.lagda.md

@@ -11,8 +11,6 @@ open import category-theory.large-precategories
 open import category-theory.maps-precategories
 open import category-theory.precategories
 
-open import foundation.contractible-types
-open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
 open import foundation.torsorial-type-families

src/category-theory/maps-set-magmoids.lagda.md

@@ -7,24 +7,13 @@ module category-theory.maps-set-magmoids where
 <details><summary>Imports</summary>
 
 ```agda
-open import category-theory.commuting-squares-of-morphisms-in-set-magmoids
 open import category-theory.set-magmoids
 
 open import foundation.action-on-identifications-functions
-open import foundation.binary-transport
 open import foundation.commuting-pentagons-of-identifications
-open import foundation.contractible-types
 open import foundation.dependent-pair-types
-open import foundation.equality-dependent-function-types
-open import foundation.equivalences
 open import foundation.function-types
-open import foundation.functoriality-dependent-pair-types
-open import foundation.fundamental-theorem-of-identity-types
-open import foundation.homotopies
-open import foundation.homotopy-induction
 open import foundation.identity-types
-open import foundation.structure-identity-principle
-open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 

src/category-theory/monomorphisms-in-large-precategories.lagda.md

@@ -10,10 +10,8 @@ module category-theory.monomorphisms-in-large-precategories where
 open import category-theory.isomorphisms-in-large-precategories
 open import category-theory.large-precategories
 
-open import foundation.action-on-identifications-functions
 open import foundation.embeddings
 open import foundation.equivalences
-open import foundation.identity-types
 open import foundation.propositions
 open import foundation.universe-levels
 ```

src/category-theory/natural-transformations-functors-large-categories.lagda.md

@@ -11,8 +11,6 @@ open import category-theory.functors-large-categories
 open import category-theory.large-categories
 open import category-theory.natural-transformations-functors-large-precategories
 
-open import foundation.action-on-identifications-functions
-open import foundation.identity-types
 open import foundation.universe-levels
 ```
 

src/category-theory/replete-subprecategories.lagda.md

@@ -14,15 +14,13 @@ open import category-theory.isomorphisms-in-subprecategories
 open import category-theory.precategories
 open import category-theory.subprecategories
 
-open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.functoriality-dependent-pair-types
 open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.subsingleton-induction
 open import foundation.subtypes
-open import foundation.transport-along-identifications
 open import foundation.type-arithmetic-cartesian-product-types
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels

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

@@ -14,7 +14,6 @@ open import category-theory.natural-transformations-functors-large-precategories
 open import foundation.category-of-sets
 open import foundation.function-extensionality
 open import foundation.function-types
-open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.sets
 open import foundation.universe-levels

src/category-theory/set-magmoids.lagda.md

@@ -22,7 +22,7 @@ open import foundation.universe-levels
 
 ## Idea
 
-A **set-magmoid** is simply the [structure](foundation.structure.md) of a
+A **set-magmoid** is the [structure](foundation.structure.md) of a
 [composition operation on a binary family of sets](category-theory.composition-operations-on-binary-families-of-sets.md),
 and are in one sense the "oidification" of [magmas](structured-types.magmas.md)
 in [sets](foundation-core.sets.md). We call elements of the indexing type

src/category-theory/structure-equivalences-set-magmoids.lagda.md

@@ -10,28 +10,16 @@ module category-theory.structure-equivalences-set-magmoids where
 open import category-theory.functors-set-magmoids
 open import category-theory.set-magmoids
 
-open import foundation.binary-equivalences
 open import foundation.cartesian-product-types
-open import foundation.contractible-types
 open import foundation.dependent-pair-types
-open import foundation.equality-dependent-function-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-dependent-pair-types
-open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
 open import foundation.iterated-dependent-product-types
 open import foundation.propositions
-open import foundation.sets
-open import foundation.structure-identity-principle
-open import foundation.subtype-identity-principle
-open import foundation.subtypes
-open import foundation.torsorial-type-families
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.type-theoretic-principle-of-choice
-open import foundation.univalence
 open import foundation.universe-levels
 ```
 

src/category-theory/subcategories.lagda.md

@@ -25,7 +25,6 @@ open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.functoriality-dependent-pair-types
 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
@@ -38,7 +37,7 @@ open import foundation.universe-levels
 
 ## Idea
 
-A **subcategory** of a [category](category-theory.categories.md) `C` is simply a
+A **subcategory** of a [category](category-theory.categories.md) `C` is a
 [subprecategory](category-theory.subprecategories.md). It consists of a
 [subtype](foundation-core.subtypes.md) `P₀` of the objects of `C`, and a family
 of subtypes

src/category-theory/yoneda-lemma-precategories.lagda.md

@@ -9,11 +9,8 @@ module category-theory.yoneda-lemma-precategories where
 ```agda
 open import category-theory.copresheaf-categories
 open import category-theory.functors-from-small-to-large-precategories
-open import category-theory.functors-precategories
 open import category-theory.natural-transformations-functors-from-small-to-large-precategories
-open import category-theory.natural-transformations-functors-precategories
 open import category-theory.precategories
-open import category-theory.presheaf-categories
 open import category-theory.representable-functors-precategories
 
 open import foundation.action-on-identifications-functions

src/commutative-algebra/groups-of-units-commutative-rings.lagda.md

@@ -14,7 +14,6 @@ open import commutative-algebra.homomorphisms-commutative-rings
 open import commutative-algebra.precategory-of-commutative-rings
 
 open import foundation.dependent-pair-types
-open import foundation.function-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.subtypes
@@ -30,9 +29,6 @@ open import group-theory.semigroups
 open import group-theory.submonoids
 
 open import ring-theory.groups-of-units-rings
-open import ring-theory.homomorphisms-rings
-open import ring-theory.invertible-elements-rings
-open import ring-theory.rings
 ```
 
 </details>

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

@@ -11,8 +11,6 @@ open import commutative-algebra.commutative-rings
 open import commutative-algebra.homomorphisms-commutative-semirings
 open import commutative-algebra.invertible-elements-commutative-rings
 
-open import foundation.contractible-types
-open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
 open import foundation.propositions

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

@@ -9,8 +9,6 @@ module commutative-algebra.homomorphisms-commutative-semirings where
 ```agda
 open import commutative-algebra.commutative-semirings
 
-open import foundation.contractible-types
-open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
 open import foundation.sets

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

@@ -13,7 +13,6 @@ open import commutative-algebra.subsets-commutative-rings
 
 open import elementary-number-theory.natural-numbers
 
-open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types

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

@@ -14,7 +14,6 @@ open import commutative-algebra.homomorphisms-commutative-rings
 open import commutative-algebra.invertible-elements-commutative-rings
 open import commutative-algebra.precategory-of-commutative-rings
 
-open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.function-types

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

@@ -11,7 +11,6 @@ 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.function-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.subtypes

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

@@ -14,7 +14,6 @@ open import commutative-algebra.subsets-commutative-rings
 
 open import elementary-number-theory.natural-numbers
 
-open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.fundamental-theorem-of-identity-types

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

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

src/elementary-number-theory/decidable-total-order-standard-finite-types.lagda.md

@@ -7,7 +7,6 @@ module elementary-number-theory.decidable-total-order-standard-finite-types wher
 <details><summary>Imports</summary>
 
 ```agda
-open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.inequality-standard-finite-types
 open import elementary-number-theory.natural-numbers
 
@@ -17,8 +16,6 @@ open import foundation.universe-levels
 
 open import order-theory.decidable-total-orders
 open import order-theory.total-orders
-
-open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>

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

@@ -9,10 +9,8 @@ module elementary-number-theory.equality-integers where
 ```agda
 open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.integers
-open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions
-open import foundation.contractible-types
 open import foundation.coproduct-types
 open import foundation.decidable-equality
 open import foundation.decidable-types

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

@@ -18,7 +18,6 @@ open import foundation.empty-types
 open import foundation.equivalences
 open import foundation.function-types
 open import foundation.fundamental-theorem-of-identity-types
-open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.set-truncations

src/elementary-number-theory/eulers-totient-function.lagda.md

@@ -11,11 +11,6 @@ module elementary-number-theory.eulers-totient-function where
 ```agda
 open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.relatively-prime-natural-numbers
-open import elementary-number-theory.sums-of-natural-numbers
-
-open import foundation.coproduct-types
-open import foundation.decidable-types
-open import foundation.dependent-pair-types
 
 open import univalent-combinatorics.decidable-subtypes
 open import univalent-combinatorics.finite-types

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

@@ -25,7 +25,6 @@ open import foundation.universe-levels
 
 open import order-theory.posets
 open import order-theory.preorders
-open import order-theory.total-orders
 
 open import univalent-combinatorics.standard-finite-types
 ```