Update src/foundation/universal-property-propositional-truncation.lag…

…da.md
UniMath · Dec 10, 2023 · 85d1f4b · 85d1f4b
1 parent 08e7319
commit 85d1f4b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/foundation/universal-property-propositional-truncation.lagda.md b/src/foundation/universal-property-propositional-truncation.lagda.md
@@ -133,7 +133,7 @@ abstract
     {l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) →
     (is-ptr-f : is-propositional-truncation P f) →
     (Q : Prop l3) (g : A → type-Prop Q) →
-    ((map-is-propositional-truncation P f is-ptr-f Q g) ∘ f) ~ g
+    map-is-propositional-truncation P f is-ptr-f Q g ∘ f ~ g
   htpy-is-propositional-truncation P f is-ptr-f Q g =
     pr2
       ( center