Update src/category-theory/indiscrete-precategories.lagda.md

UniMath · Nov 24, 2023 · 8c5e976 · 8c5e976
1 parent 48ef93f
commit 8c5e976
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/category-theory/indiscrete-precategories.lagda.md b/src/category-theory/indiscrete-precategories.lagda.md
@@ -46,7 +46,7 @@ hom-[sets](foundation-core.sets.md) are
 This construction demonstrates one essential aspect about precategories: While
 it displays `obj-Precategory` as a [retraction](foundation-core.retractions.md),
 every indiscrete precategory is
-[subterminal](category-theory.subterminal-precategories.lagda.md).
+[subterminal](category-theory.subterminal-precategories.md).
 
 ## Definitions