From 85d1f4b5b8edd47ba6a0593f7936756a3ff94921 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 10 Dec 2023 01:49:15 +0100 Subject: [PATCH] Update src/foundation/universal-property-propositional-truncation.lagda.md --- .../universal-property-propositional-truncation.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation/universal-property-propositional-truncation.lagda.md b/src/foundation/universal-property-propositional-truncation.lagda.md index 4e71235313..e506ee07d6 100644 --- 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