diff --git a/src/finite-group-theory/concrete-quaternion-group.lagda.md b/src/finite-group-theory/concrete-quaternion-group.lagda.md
index 9087543aad..c7c9128a36 100644
--- a/src/finite-group-theory/concrete-quaternion-group.lagda.md
+++ b/src/finite-group-theory/concrete-quaternion-group.lagda.md
@@ -37,7 +37,7 @@ equiv-face-cube :
       ( map-axis-equiv-cube (succ-ℕ k) X Y e d a))
 equiv-face-cube k X Y e d a =
   pair
-    ( equiv-complement-point-UU-Fin k
+    ( equiv-complement-element-UU-Fin k
       ( pair (dim-cube-UU-Fin (succ-ℕ k) X) d)
       ( pair
         ( dim-cube-UU-Fin (succ-ℕ k) Y)
@@ -48,7 +48,7 @@ equiv-face-cube k X Y e d a =
       ( equiv-tr
         ( axis-cube (succ-ℕ k) Y)
         ( inv
-          ( natural-inclusion-equiv-complement-isolated-point
+          ( natural-inclusion-equiv-complement-isolated-element
             ( dim-equiv-cube (succ-ℕ k) X Y e)
             ( pair d
               ( λ z →
@@ -68,7 +68,7 @@ equiv-face-cube k X Y e d a =
             ( refl)
             ( d')))) ∘e
       ( axis-equiv-cube (succ-ℕ k) X Y e
-        ( inclusion-complement-point-UU-Fin k
+        ( inclusion-complement-element-UU-Fin k
           ( pair (dim-cube-UU-Fin (succ-ℕ k) X) d) d')))
 
 cube-with-labeled-faces :
diff --git a/src/foundation/isolated-elements.lagda.md b/src/foundation/isolated-elements.lagda.md
index 31fe2e98df..56439d9694 100644
--- a/src/foundation/isolated-elements.lagda.md
+++ b/src/foundation/isolated-elements.lagda.md
@@ -69,7 +69,7 @@ module _
   is-isolated-isolated-element = pr2 x
 ```
 
-### Complements of isolated points
+### Complements of isolated elements
 
 ```agda
 complement-isolated-element :
@@ -162,7 +162,8 @@ module _
 
     is-contr-total-Eq-isolated-element :
       (d : is-isolated a) → is-contr (Σ A (Eq-isolated-element d))
-    pr1 (is-contr-total-Eq-isolated-element d) = center-total-Eq-isolated-element d
+    pr1 (is-contr-total-Eq-isolated-element d) =
+      center-total-Eq-isolated-element d
     pr2 (is-contr-total-Eq-isolated-element d) =
       contraction-total-Eq-isolated-element d
 
@@ -280,7 +281,7 @@ module _
     is-decidable-emb-point-isolated-element
 ```
 
-### Types with isolated points can be equipped with a Maybe-structure
+### Types with isolated elements can be equipped with a Maybe-structure
 
 ```agda
 map-maybe-structure-isolated-element :
diff --git a/src/foundation/products-unordered-tuples-of-types.lagda.md b/src/foundation/products-unordered-tuples-of-types.lagda.md
index 0d38144963..b0be1de823 100644
--- a/src/foundation/products-unordered-tuples-of-types.lagda.md
+++ b/src/foundation/products-unordered-tuples-of-types.lagda.md
@@ -53,14 +53,14 @@ equiv-pr-product-unordered-tuple-types :
 equiv-pr-product-unordered-tuple-types n A i =
   ( equiv-Π
     ( element-unordered-tuple (succ-ℕ n) A)
-    ( equiv-maybe-structure-point-UU-Fin n
+    ( equiv-maybe-structure-element-UU-Fin n
       ( type-unordered-tuple-UU-Fin (succ-ℕ n) A) i)
     ( λ x → id-equiv)) ∘e
   ( inv-equiv
     ( equiv-dependent-universal-property-Maybe
       ( λ j →
         element-unordered-tuple (succ-ℕ n) A
-          ( map-equiv (equiv-maybe-structure-point-UU-Fin n
+          ( map-equiv (equiv-maybe-structure-element-UU-Fin n
             ( type-unordered-tuple-UU-Fin (succ-ℕ n) A) i)
             ( j)))))
 
diff --git a/src/foundation/unordered-tuples.lagda.md b/src/foundation/unordered-tuples.lagda.md
index 4693c07116..ac5fa9d23b 100644
--- a/src/foundation/unordered-tuples.lagda.md
+++ b/src/foundation/unordered-tuples.lagda.md
@@ -84,7 +84,7 @@ module _
 
   type-complement-point-unordered-tuple-UU-Fin : UU-Fin lzero n
   type-complement-point-unordered-tuple-UU-Fin =
-    complement-point-UU-Fin n
+    complement-element-UU-Fin n
       ( pair (type-unordered-tuple-UU-Fin (succ-ℕ n) t) i)
 
   type-complement-point-unordered-tuple : UU lzero
@@ -94,13 +94,13 @@ module _
   inclusion-complement-point-unordered-tuple :
     type-complement-point-unordered-tuple → type-unordered-tuple (succ-ℕ n) t
   inclusion-complement-point-unordered-tuple =
-    inclusion-complement-point-UU-Fin n
+    inclusion-complement-element-UU-Fin n
       ( pair (type-unordered-tuple-UU-Fin (succ-ℕ n) t) i)
 
   unordered-tuple-complement-point-type-unordered-tuple :
     unordered-tuple n A
   pr1 unordered-tuple-complement-point-type-unordered-tuple =
-    complement-point-UU-Fin n
+    complement-element-UU-Fin n
       ( pair (type-unordered-tuple-UU-Fin (succ-ℕ n) t) i)
   pr2 unordered-tuple-complement-point-type-unordered-tuple =
     ( element-unordered-tuple (succ-ℕ n) t) ∘
diff --git a/src/univalent-combinatorics.lagda.md b/src/univalent-combinatorics.lagda.md
index 9764775769..008ad5b3b2 100644
--- a/src/univalent-combinatorics.lagda.md
+++ b/src/univalent-combinatorics.lagda.md
@@ -27,7 +27,7 @@ open import univalent-combinatorics.binomial-types public
 open import univalent-combinatorics.bracelets public
 open import univalent-combinatorics.cartesian-product-types public
 open import univalent-combinatorics.classical-finite-types public
-open import univalent-combinatorics.complements-isolated-points public
+open import univalent-combinatorics.complements-isolated-elements public
 open import univalent-combinatorics.coproduct-types public
 open import univalent-combinatorics.counting public
 open import univalent-combinatorics.counting-decidable-subtypes public
diff --git a/src/univalent-combinatorics/complements-isolated-points.lagda.md b/src/univalent-combinatorics/complements-isolated-elements.lagda.md
similarity index 60%
rename from src/univalent-combinatorics/complements-isolated-points.lagda.md
rename to src/univalent-combinatorics/complements-isolated-elements.lagda.md
index c7e95b4b85..d0893d63cb 100644
--- a/src/univalent-combinatorics/complements-isolated-points.lagda.md
+++ b/src/univalent-combinatorics/complements-isolated-elements.lagda.md
@@ -1,4 +1,4 @@
-# Complements of isolated points of finite types
+# Complements of isolated elements of finite types
 
 ```agda
 module univalent-combinatorics.complements-isolated-elements where
@@ -26,89 +26,89 @@ open import univalent-combinatorics.finite-types
 
 ## Idea
 
-For any point `x` in a [finite type](univalent-combinatorics.finite-types.md)
+For any element `x` in a [finite type](univalent-combinatorics.finite-types.md)
 `X` of [cardinality](set-theory.cardinalities.md) `n+1`, we can construct its
 **complement**, which is a type of cardinality `n`.
 
 ## Definition
 
-### The complement of a point in a k-element type of arbitrary universe level
+### The complement of a element in a `k`-element type of arbitrary universe level
 
 ```agda
-isolated-point-UU-Fin :
+isolated-element-UU-Fin :
   {l : Level} (k : ℕ) (X : UU-Fin l (succ-ℕ k)) →
   type-UU-Fin (succ-ℕ k) X →
-  isolated-point (type-UU-Fin (succ-ℕ k) X)
-pr1 (isolated-point-UU-Fin k X x) = x
-pr2 (isolated-point-UU-Fin k X x) =
+  isolated-element (type-UU-Fin (succ-ℕ k) X)
+pr1 (isolated-element-UU-Fin k X x) = x
+pr2 (isolated-element-UU-Fin k X x) =
   has-decidable-equality-has-cardinality
     ( succ-ℕ k)
     ( has-cardinality-type-UU-Fin (succ-ℕ k) X)
     ( x)
 
-type-complement-point-UU-Fin :
+type-complement-element-UU-Fin :
   {l1 : Level} (k : ℕ) →
   Σ (UU-Fin l1 (succ-ℕ k)) (type-UU-Fin (succ-ℕ k)) → UU l1
-type-complement-point-UU-Fin k (X , x) =
-  complement-isolated-point
+type-complement-element-UU-Fin k (X , x) =
+  complement-isolated-element
     ( type-UU-Fin (succ-ℕ k) X)
-    ( isolated-point-UU-Fin k X x)
+    ( isolated-element-UU-Fin k X x)
 
-equiv-maybe-structure-point-UU-Fin :
+equiv-maybe-structure-element-UU-Fin :
   {l : Level} (k : ℕ) (X : UU-Fin l (succ-ℕ k)) →
   (x : type-UU-Fin (succ-ℕ k) X) →
-  Maybe (type-complement-point-UU-Fin k (pair X x)) ≃
+  Maybe (type-complement-element-UU-Fin k (pair X x)) ≃
   type-UU-Fin (succ-ℕ k) X
-equiv-maybe-structure-point-UU-Fin k X x =
-  equiv-maybe-structure-isolated-point
+equiv-maybe-structure-element-UU-Fin k X x =
+  equiv-maybe-structure-isolated-element
     ( type-UU-Fin (succ-ℕ k) X)
-    ( isolated-point-UU-Fin k X x)
+    ( isolated-element-UU-Fin k X x)
 
-has-cardinality-type-complement-point-UU-Fin :
+has-cardinality-type-complement-element-UU-Fin :
   {l1 : Level} (k : ℕ)
   (X : Σ (UU-Fin l1 (succ-ℕ k)) (type-UU-Fin (succ-ℕ k))) →
-  has-cardinality k (type-complement-point-UU-Fin k X)
-has-cardinality-type-complement-point-UU-Fin k (pair (pair X H) x) =
+  has-cardinality k (type-complement-element-UU-Fin k X)
+has-cardinality-type-complement-element-UU-Fin k (pair (pair X H) x) =
   apply-universal-property-trunc-Prop H
     ( has-cardinality-Prop k
-      ( type-complement-point-UU-Fin k (pair (pair X H) x)))
+      ( type-complement-element-UU-Fin k (pair (pair X H) x)))
     ( λ e →
       unit-trunc-Prop
         ( equiv-equiv-Maybe
           ( ( inv-equiv
-              ( equiv-maybe-structure-point-UU-Fin k (pair X H) x)) ∘e
+              ( equiv-maybe-structure-element-UU-Fin k (pair X H) x)) ∘e
             ( e))))
 
-complement-point-UU-Fin :
+complement-element-UU-Fin :
   {l1 : Level} (k : ℕ) →
   Σ (UU-Fin l1 (succ-ℕ k)) (type-UU-Fin (succ-ℕ k)) →
   UU-Fin l1 k
-pr1 (complement-point-UU-Fin k T) =
-  type-complement-point-UU-Fin k T
-pr2 (complement-point-UU-Fin k T) =
-  has-cardinality-type-complement-point-UU-Fin k T
+pr1 (complement-element-UU-Fin k T) =
+  type-complement-element-UU-Fin k T
+pr2 (complement-element-UU-Fin k T) =
+  has-cardinality-type-complement-element-UU-Fin k T
 
-inclusion-complement-point-UU-Fin :
+inclusion-complement-element-UU-Fin :
   {l1 : Level} (k : ℕ)
   (X : Σ (UU-Fin l1 (succ-ℕ k)) (type-UU-Fin (succ-ℕ k))) →
-  type-complement-point-UU-Fin k X → type-UU-Fin (succ-ℕ k) (pr1 X)
-inclusion-complement-point-UU-Fin k X x = pr1 x
+  type-complement-element-UU-Fin k X → type-UU-Fin (succ-ℕ k) (pr1 X)
+inclusion-complement-element-UU-Fin k X x = pr1 x
 ```
 
 ### The action of equivalences on complements of isolated points
 
 ```agda
-equiv-complement-point-UU-Fin :
+equiv-complement-element-UU-Fin :
   {l1 : Level} (k : ℕ)
   (X Y : Σ (UU-Fin l1 (succ-ℕ k)) (type-UU-Fin (succ-ℕ k))) →
   (e : equiv-UU-Fin (succ-ℕ k) (pr1 X) (pr1 Y))
   (p : Id (map-equiv e (pr2 X)) (pr2 Y)) →
   equiv-UU-Fin k
-    ( complement-point-UU-Fin k X)
-    ( complement-point-UU-Fin k Y)
-equiv-complement-point-UU-Fin
+    ( complement-element-UU-Fin k X)
+    ( complement-element-UU-Fin k Y)
+equiv-complement-element-UU-Fin
   k S T e p =
-  equiv-complement-isolated-point e
+  equiv-complement-isolated-element e
     ( pair x (λ x' → has-decidable-equality-has-cardinality (succ-ℕ k) H x x'))
     ( pair y (λ y' → has-decidable-equality-has-cardinality (succ-ℕ k) K y y'))
     ( p)
@@ -121,7 +121,7 @@ equiv-complement-point-UU-Fin
 
 ## Properties
 
-### The map from a pointed `k+1`-element type to the complement of the point is an equivalence
+### The map from a pointed `k+1`-element type to the complement of the element is an equivalence
 
 This remains to be shown.
 [#744](https://github.com/UniMath/agda-unimath/issues/744)
diff --git a/src/univalent-combinatorics/cubes.lagda.md b/src/univalent-combinatorics/cubes.lagda.md
index 3481ec791c..0c9ea342e7 100644
--- a/src/univalent-combinatorics/cubes.lagda.md
+++ b/src/univalent-combinatorics/cubes.lagda.md
@@ -106,9 +106,9 @@ face-cube :
   (k : ℕ) (X : cube (succ-ℕ k)) (d : dim-cube (succ-ℕ k) X)
   (a : axis-cube (succ-ℕ k) X d) → cube k
 pr1 (face-cube k X d a) =
-  complement-point-UU-Fin k (pair (dim-cube-UU-Fin (succ-ℕ k) X) d)
+  complement-element-UU-Fin k (pair (dim-cube-UU-Fin (succ-ℕ k) X) d)
 pr2 (face-cube k X d a) d' =
   axis-cube-UU-2 (succ-ℕ k) X
-    ( inclusion-complement-point-UU-Fin k
+    ( inclusion-complement-element-UU-Fin k
       ( pair (dim-cube-UU-Fin (succ-ℕ k) X) d) d')
 ```
diff --git a/src/univalent-combinatorics/main-classes-of-latin-hypercubes.lagda.md b/src/univalent-combinatorics/main-classes-of-latin-hypercubes.lagda.md
index c09d8837d1..dee4973e2e 100644
--- a/src/univalent-combinatorics/main-classes-of-latin-hypercubes.lagda.md
+++ b/src/univalent-combinatorics/main-classes-of-latin-hypercubes.lagda.md
@@ -122,7 +122,7 @@ is-π-finite-Main-Class-Latin-Hypercube-of-Order k n m =
                 is-finite-Π
                   ( is-finite-Π
                     ( is-finite-has-cardinality n
-                      ( has-cardinality-type-complement-point-UU-Fin n
+                      ( has-cardinality-type-complement-element-UU-Fin n
                         ( pair (type-unordered-tuple-UU-Fin (succ-ℕ n) A) i)))
                     ( λ j →
                       is-finite-type-UU-Fin m