fix imports

UniMath · Dec 6, 2023 · 8f3bc5f · 8f3bc5f
1 parent 53c2cb0
commit 8f3bc5f
Show file tree

Hide file tree

Showing 5 changed files with 4 additions and 6 deletions.
diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md
@@ -30,7 +30,7 @@ open import foundation-core.fibers-of-maps public
 open import foundation-core.function-extensionality public
 open import foundation-core.function-types public
 open import foundation-core.functoriality-dependent-function-types public
-open import foundation-core.functoriality-dependent-pair-types public public
+open import foundation-core.functoriality-dependent-pair-types public
 open import foundation-core.homotopies public
 open import foundation-core.identity-types public
 open import foundation-core.injective-maps public

diff --git a/src/foundation-core/commuting-triangles-of-maps.lagda.md b/src/foundation-core/commuting-triangles-of-maps.lagda.md
@@ -8,10 +8,10 @@ module foundation-core.commuting-triangles-of-maps where
 
 ```agda
 open import foundation.universe-levels
-open import foundation-core.precomposition-functions
 
 open import foundation-core.function-types
 open import foundation-core.homotopies
+open import foundation-core.precomposition-functions
 open import foundation-core.retractions
 open import foundation-core.sections
 open import foundation-core.whiskering-homotopies

diff --git a/src/foundation/commuting-squares-of-maps.lagda.md b/src/foundation/commuting-squares-of-maps.lagda.md
@@ -12,8 +12,8 @@ open import foundation-core.commuting-squares-of-maps public
 open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-squares-of-homotopies
-open import foundation.commuting-triangles-of-maps
 open import foundation.commuting-squares-of-identifications
+open import foundation.commuting-triangles-of-maps
 open import foundation.equivalences
 open import foundation.path-algebra
 open import foundation.precomposition-dependent-functions
@@ -22,7 +22,6 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies
 
 open import foundation-core.commuting-prisms-of-maps
-open import foundation-core.commuting-triangles-of-maps
 open import foundation-core.function-extensionality
 open import foundation-core.function-types
 open import foundation-core.homotopies

diff --git a/src/foundation/commuting-triangles-of-maps.lagda.md b/src/foundation/commuting-triangles-of-maps.lagda.md
@@ -10,7 +10,6 @@ open import foundation-core.commuting-triangles-of-maps public
 
 ```agda
 open import foundation.action-on-identifications-functions
-open import foundation-core.function-extensionality
 open import foundation.functoriality-dependent-function-types
 open import foundation.homotopies
 open import foundation.identity-types
@@ -19,6 +18,7 @@ open import foundation.precomposition-functions
 open import foundation.universe-levels
 
 open import foundation-core.equivalences
+open import foundation-core.function-extensionality
 open import foundation-core.function-types
 ```
 

diff --git a/tables/composition.md b/tables/composition.md
@@ -16,7 +16,6 @@
 | Functoriality of dependent function types                   | [`foundation.functoriality-dependent-function-types`](foundation.functoriality-dependent-function-types.md)           |
 | Functoriality of dependent function types (foundation-core) | [`foundation-core.functoriality-dependent-function-types`](foundation-core.functoriality-dependent-function-types.md) |
 | Functoriality of function types                             | [`foundation.functoriality-function-types`](foundation.functoriality-function-types.md)                               |
-| Functoriality of function types (foundation-core)           | [`foundation-core.functoriality-function-types`](foundation-core.functoriality-function-types.md)                     |
 | Implicit function types                                     | [`foundation.implicit-function-types`](foundation.implicit-function-types.md)                                         |
 | Iterating functions                                         | [`foundation.iterating-functions`](foundation.iterating-functions.md)                                                 |
 | Postcomposition                                             | [`foundation.postcomposition`](foundation.postcomposition-functions.md)                                               |