From ce8b02941df37bff09264b77d8ab672b64f3e367 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Sun, 22 Oct 2023 18:28:06 +0200 Subject: [PATCH] fix link --- src/foundation-core/homotopies.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation-core/homotopies.lagda.md b/src/foundation-core/homotopies.lagda.md index e02e9610ca..42205ec1a9 100644 --- a/src/foundation-core/homotopies.lagda.md +++ b/src/foundation-core/homotopies.lagda.md @@ -335,7 +335,7 @@ syntax step-homotopy-reasoning p h q = p ~ h by q - We postulate that homotopies characterize identifications of (dependent) functions in the file - [`foundation.function-extensionality`](foundation-core.function-extensionality.md). + [`foundation.function-extensionality`](foundation.function-extensionality.md). - [Multivariable homotopies](foundation.multivariable-homotopies.md). - The [whiskering operations](foundation.whiskering-homotopies.md) on homotopies.