pre-commit

UniMath · Dec 8, 2023 · f3d7ec4 · f3d7ec4
1 parent 0e800e0
commit f3d7ec4
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 5 deletions.
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
@@ -219,6 +219,7 @@ open import foundation.multivariable-homotopies public
 open import foundation.multivariable-operations public
 open import foundation.multivariable-relations public
 open import foundation.multivariable-sections public
+open import foundation.my-file-about-computing-htpy-precomp public
 open import foundation.negated-equality public
 open import foundation.negation public
 open import foundation.noncontractible-types public

diff --git a/src/foundation/commuting-prisms-of-maps.lagda.md b/src/foundation/commuting-prisms-of-maps.lagda.md
@@ -15,8 +15,8 @@ open import foundation.commuting-squares-of-maps
 open import foundation.commuting-triangles-of-maps
 open import foundation.function-extensionality
 open import foundation.identity-types
-open import foundation.path-algebra
 open import foundation.my-file-about-computing-htpy-precomp
+open import foundation.path-algebra
 open import foundation.precomposition-functions
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies

diff --git a/src/foundation/my-file-about-computing-htpy-precomp.lagda.md b/src/foundation/my-file-about-computing-htpy-precomp.lagda.md
@@ -7,16 +7,16 @@ module foundation.my-file-about-computing-htpy-precomp where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.precomposition-functions
 open import foundation.universe-levels
 
 open import foundation-core.commuting-squares-of-maps
 open import foundation-core.commuting-triangles-of-maps
 open import foundation-core.homotopies
 open import foundation-core.whiskering-homotopies
-open import foundation.function-types
-open import foundation.action-on-identifications-functions
-open import foundation.precomposition-functions
-open import foundation.function-extensionality
 ```
 
 </details>