rename isolated points to isolated elements

UniMath · Oct 8, 2023 · 5b29ac1 · 5b29ac1
1 parent e1affd9
commit 5b29ac1
Show file tree

Hide file tree

Showing 14 changed files with 406 additions and 400 deletions.
diff --git a/src/finite-group-theory/concrete-quaternion-group.lagda.md b/src/finite-group-theory/concrete-quaternion-group.lagda.md
@@ -12,11 +12,11 @@ open import elementary-number-theory.natural-numbers
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
-open import foundation.isolated-points
+open import foundation.isolated-elements
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
-open import univalent-combinatorics.complements-isolated-points
+open import univalent-combinatorics.complements-isolated-elements
 open import univalent-combinatorics.cubes
 open import univalent-combinatorics.equality-finite-types
 open import univalent-combinatorics.equivalences-cubes

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
@@ -158,7 +158,7 @@ open import foundation.interchange-law public
 open import foundation.intersections-subtypes public
 open import foundation.invertible-maps public
 open import foundation.involutions public
-open import foundation.isolated-points public
+open import foundation.isolated-elements public
 open import foundation.isomorphisms-of-sets public
 open import foundation.iterated-cartesian-product-types public
 open import foundation.iterating-automorphisms public