diff --git a/src/foundation/univalence.lagda.md b/src/foundation/univalence.lagda.md
index e0804edd00..f175d248cb 100644
--- a/src/foundation/univalence.lagda.md
+++ b/src/foundation/univalence.lagda.md
@@ -86,7 +86,7 @@ module _
     is-contr-total-equiv :
       (A : UU l) → is-contr (Σ (UU l) (λ X → A ≃ X))
     is-contr-total-equiv A =
-      is-contr-total-equiv-univalence A (univalence A)
+      is-contr-total-equiv-based-univalence A (univalence A)
 
     is-contr-total-equiv' :
       (A : UU l) → is-contr (Σ (UU l) (λ X → X ≃ A))