oops

UniMath · Oct 20, 2023 · a6dfec0 · a6dfec0
1 parent 09837f5
commit a6dfec0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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))