diff --git a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md
index f46c4bbfa4..68d89269b2 100644
--- a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md
+++ b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md
@@ -40,8 +40,8 @@ open import synthetic-homotopy-theory.powers-of-loops
 ## Idea
 
 **Hatcher's [acyclic type](synthetic-homotopy-theory.acyclic-types.md)** is a
-higher inductive type [equipped](foundation.structure.md) with a base point and two
-[loops](synthetic-homotopy-theory.loop-spaces.md) `a` and `b`, and
+higher inductive type [equipped](foundation.structure.md) with a base point and
+two [loops](synthetic-homotopy-theory.loop-spaces.md) `a` and `b`, and
 [identifications](foundation.identity-types.md) witnessing that `a⁵ ＝ b³` and
 `b³ = (ab)²`. This type is acyclic, because the structure on Hatcher's acyclic
 type on any loop space is [contractible](foundation.contractible-types.md).