Remove dependency between BUILTIN and postulates

scripts/remove_unused_imports.py

@@ -115,7 +115,7 @@ def filter_agda_files(f): return utils.is_agda_file(pathlib.Path(f)) and os.path
 
     temp_dir = 'temp'
     status = 0
-    agda_options = '--without-K --exact-split --no-import-sorts --auto-inline --no-caching'
+    agda_options = '--without-K --exact-split --no-import-sorts --auto-inline --no-caching -WnoPatternShadowsConstructor'
 
     temp_root = os.path.join(root, temp_dir)
     shutil.rmtree(temp_root, ignore_errors=True)

src/category-theory/categories.lagda.md

@@ -17,6 +17,7 @@ open import category-theory.strongly-preunivalent-categories
 open import foundation.1-types
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.equivalences
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types

src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md

@@ -9,13 +9,15 @@ module category-theory.composition-operations-on-binary-families-of-sets where
 ```agda
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.function-extensionality
 open import foundation.identity-types
 open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.sets
 open import foundation.strictly-involutive-identity-types
 open import foundation.subtypes
+open import foundation.telescopes
 open import foundation.universe-levels
 ```
 

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

@@ -22,6 +22,8 @@ open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.dependent-identifications
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-contractible-types
+open import foundation.dependent-products-propositions
 open import foundation.equality-dependent-function-types
 open import foundation.equality-dependent-pair-types
 open import foundation.equivalences

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

@@ -12,8 +12,10 @@ open import category-theory.isomorphisms-in-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.iterated-dependent-product-types
 open import foundation.propositions
+open import foundation.telescopes
 open import foundation.universe-levels
 ```
 

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

@@ -19,6 +19,7 @@ open import category-theory.precategories
 open import category-theory.precategory-of-functors
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.equality-dependent-pair-types
 open import foundation.homotopies
 open import foundation.identity-types

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

@@ -24,18 +24,22 @@ open import category-theory.terminal-objects-precategories
 open import foundation.category-of-sets
 open import foundation.commuting-squares-of-maps
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.empty-types
 open import foundation.equality-cartesian-product-types
 open import foundation.function-extensionality
+open import foundation.function-extensionality-axiom
 open import foundation.function-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
-open import foundation.raising-universe-levels
+open import foundation.raising-universe-levels-unit-type
 open import foundation.sets
 open import foundation.unit-type
 open import foundation.universe-levels
+
+open import foundation-core.raising-universe-levels
 ```
 
 </details>

src/category-theory/coproducts-in-precategories.lagda.md

@@ -13,9 +13,12 @@ open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-contractible-types
+open import foundation.dependent-products-propositions
 open import foundation.identity-types
 open import foundation.iterated-dependent-product-types
 open import foundation.propositions
+open import foundation.telescopes
 open import foundation.uniqueness-quantification
 open import foundation.universe-levels
 ```

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

@@ -18,6 +18,7 @@ open import category-theory.wide-subprecategories
 
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-contractible-types
 open import foundation.equivalences
 open import foundation.functoriality-dependent-pair-types
 open import foundation.fundamental-theorem-of-identity-types

src/category-theory/dependent-composition-operations-over-precategories.lagda.md

@@ -15,11 +15,14 @@ open import category-theory.set-magmoids
 open import foundation.cartesian-product-types
 open import foundation.dependent-identifications
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
+open import foundation.dependent-products-truncated-types
 open import foundation.function-types
 open import foundation.identity-types
 open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.sets
+open import foundation.telescopes
 open import foundation.transport-along-identifications
 open import foundation.truncated-types
 open import foundation.truncation-levels

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

@@ -11,8 +11,10 @@ open import category-theory.isomorphisms-in-large-precategories
 open import category-theory.large-precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.equivalences
 open import foundation.function-extensionality
+open import foundation.function-extensionality-axiom
 open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.propositions

src/category-theory/dependent-products-of-precategories.lagda.md

@@ -12,8 +12,10 @@ open import category-theory.isomorphisms-in-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.equivalences
 open import foundation.function-extensionality
+open import foundation.function-extensionality-axiom
 open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.propositions

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

@@ -16,6 +16,8 @@ open import category-theory.set-magmoids
 open import foundation.cartesian-product-types
 open import foundation.dependent-identifications
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
+open import foundation.dependent-products-truncated-types
 open import foundation.equality-dependent-pair-types
 open import foundation.function-types
 open import foundation.identity-types

src/category-theory/embedding-maps-precategories.lagda.md

@@ -12,6 +12,7 @@ open import category-theory.maps-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.embeddings
 open import foundation.propositions
 open import foundation.universe-levels

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

@@ -13,6 +13,7 @@ open import category-theory.maps-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.propositions
 open import foundation.universe-levels
 ```

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

@@ -10,6 +10,7 @@ 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.dependent-products-propositions
 open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.propositions

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

@@ -12,6 +12,7 @@ open import category-theory.isomorphisms-in-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.existential-quantification
 open import foundation.propositions
 open import foundation.universe-levels

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

@@ -13,6 +13,7 @@ open import category-theory.isomorphisms-in-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.propositions

src/category-theory/faithful-maps-precategories.lagda.md

@@ -11,6 +11,7 @@ open import category-theory.maps-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.function-types
@@ -19,6 +20,7 @@ open import foundation.iterated-dependent-product-types
 open import foundation.logical-equivalences
 open import foundation.propositions
 open import foundation.sets
+open import foundation.telescopes
 open import foundation.universe-levels
 ```
 

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

@@ -12,6 +12,7 @@ open import category-theory.functors-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.function-types
 open import foundation.propositions
 open import foundation.universe-levels

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

@@ -12,6 +12,7 @@ open import category-theory.functors-large-categories
 open import category-theory.large-categories
 open import category-theory.large-precategories
 
+open import foundation.dependent-products-propositions
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets

src/category-theory/full-large-subprecategories.lagda.md

@@ -13,6 +13,7 @@ open import category-theory.isomorphisms-in-large-precategories
 open import category-theory.large-categories
 open import category-theory.large-precategories
 
+open import foundation.dependent-products-propositions
 open import foundation.function-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types

src/category-theory/full-maps-precategories.lagda.md

@@ -11,10 +11,12 @@ open import category-theory.maps-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.function-types
 open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.surjective-maps
+open import foundation.telescopes
 open import foundation.universe-levels
 ```
 

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

@@ -17,6 +17,7 @@ open import category-theory.maps-categories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.embeddings
 open import foundation.identity-types
 open import foundation.propositions

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

@@ -18,6 +18,7 @@ open import category-theory.maps-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.function-types

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

@@ -20,6 +20,7 @@ open import category-theory.pseudomonic-functors-precategories
 open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.equivalences
 open import foundation.function-types
 open import foundation.identity-types

src/category-theory/fully-faithful-maps-precategories.lagda.md

@@ -13,11 +13,13 @@ open import category-theory.maps-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.equivalences
 open import foundation.function-types
 open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.surjective-maps
+open import foundation.telescopes
 open import foundation.universe-levels
 ```
 

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

@@ -12,6 +12,7 @@ open import category-theory.functors-precategories
 open import category-theory.isomorphisms-in-categories
 open import category-theory.maps-categories
 
+open import foundation.dependent-products-propositions
 open import foundation.equivalences
 open import foundation.function-types
 open import foundation.homotopies

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

@@ -15,6 +15,7 @@ open import category-theory.precategories
 
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.function-types

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

@@ -12,6 +12,7 @@ open import category-theory.set-magmoids
 
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.function-types
@@ -20,6 +21,7 @@ open import foundation.identity-types
 open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.subtypes
+open import foundation.telescopes
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
 ```

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

@@ -20,6 +20,7 @@ open import category-theory.strongly-preunivalent-categories
 
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets

src/category-theory/groupoids.lagda.md

@@ -17,6 +17,8 @@ open import category-theory.pregroupoids
 open import foundation.1-types
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-contractible-types
+open import foundation.dependent-products-propositions
 open import foundation.equivalences
 open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
@@ -26,6 +28,7 @@ open import foundation.iterated-dependent-pair-types
 open import foundation.propositions
 open import foundation.sets
 open import foundation.strictly-involutive-identity-types
+open import foundation.telescopes
 open import foundation.torsorial-type-families
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels

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

@@ -16,13 +16,16 @@ open import category-theory.subterminal-precategories
 
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-contractible-types
+open import foundation.dependent-products-propositions
 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.sets
+open import foundation.telescopes
 open import foundation.unit-type
 open import foundation.universe-levels
 ```

src/category-theory/initial-category.lagda.md

@@ -17,6 +17,7 @@ open import category-theory.strongly-preunivalent-categories
 
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-contractible-types
 open import foundation.empty-types
 open import foundation.identity-types
 open import foundation.sets

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

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

src/category-theory/initial-objects-precategories.lagda.md

@@ -11,6 +11,8 @@ open import category-theory.precategories
 
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-contractible-types
+open import foundation.dependent-products-propositions
 open import foundation.function-types
 open import foundation.propositions
 open import foundation.universe-levels

src/category-theory/isomorphisms-in-categories.lagda.md

@@ -14,6 +14,8 @@ open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-contractible-types
+open import foundation.dependent-products-propositions
 open import foundation.equivalences
 open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types

src/category-theory/isomorphisms-in-large-categories.lagda.md

@@ -13,6 +13,8 @@ open import category-theory.large-categories
 
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-contractible-types
+open import foundation.dependent-products-propositions
 open import foundation.equivalences
 open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies