diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index a50fa8e2c1..86a02a85a4 100644 --- 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 index 5401d5e158..0c6f09967a 100644 --- 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 index eb146a00a5..715977a61a 100644 --- 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
Imports ```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 ```