From 9868472935558b3ad98ca8421c4965f48d9feedf Mon Sep 17 00:00:00 2001 From: Ian Ray Date: Fri, 20 Sep 2024 11:41:57 -0400 Subject: [PATCH] 1 -> -1 --- source/UF/Truncations.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/source/UF/Truncations.lagda b/source/UF/Truncations.lagda index e5c69a44c..c1cdbaf40 100644 --- a/source/UF/Truncations.lagda +++ b/source/UF/Truncations.lagda @@ -154,7 +154,7 @@ groupoid). \end{code} We demonstrate the equivalence of one-truncation and propositional truncation: - ∥ X ∥₁ ≃ ∥ X ∥ + ∥ X ∥[ −1 ] ≃ ∥ X ∥ \begin{code}