diff --git a/src/commutative-algebra/isomorphisms-commutative-rings.lagda.md b/src/commutative-algebra/isomorphisms-commutative-rings.lagda.md
index 9fb0bb46a5..bb5a267b00 100644
--- a/src/commutative-algebra/isomorphisms-commutative-rings.lagda.md
+++ b/src/commutative-algebra/isomorphisms-commutative-rings.lagda.md
@@ -353,7 +353,7 @@ module _
 
   iso-ab-iso-ab-Commutative-Ring :
     iso-ab-Commutative-Ring →
-    type-iso-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)
+    iso-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)
   iso-ab-iso-ab-Commutative-Ring =
     iso-ab-iso-ab-Ring
       ( ring-Commutative-Ring A)
@@ -376,7 +376,7 @@ module _
 
   iso-ab-iso-Commutative-Ring :
     iso-Commutative-Ring A B →
-    type-iso-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)
+    iso-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)
   iso-ab-iso-Commutative-Ring =
     iso-ab-iso-Ring
       ( ring-Commutative-Ring A)
diff --git a/src/commutative-algebra/transporting-commutative-ring-structure-isomorphisms-abelian-groups.lagda.md b/src/commutative-algebra/transporting-commutative-ring-structure-isomorphisms-abelian-groups.lagda.md
index cecfd5ce0f..d504ae3dbc 100644
--- a/src/commutative-algebra/transporting-commutative-ring-structure-isomorphisms-abelian-groups.lagda.md
+++ b/src/commutative-algebra/transporting-commutative-ring-structure-isomorphisms-abelian-groups.lagda.md
@@ -50,7 +50,7 @@ transported ring structure.
 ```agda
 module _
   {l1 l2 : Level} (A : Commutative-Ring l1) (B : Ab l2)
-  (f : type-iso-Ab (ab-Commutative-Ring A) B)
+  (f : iso-Ab (ab-Commutative-Ring A) B)
   where
 
   ring-transport-commutative-ring-structure-iso-Ab : Ring l2
diff --git a/src/finite-group-theory/finite-type-groups.lagda.md b/src/finite-group-theory/finite-type-groups.lagda.md
index 9e5ac017b0..8c02609a86 100644
--- a/src/finite-group-theory/finite-type-groups.lagda.md
+++ b/src/finite-group-theory/finite-type-groups.lagda.md
@@ -126,7 +126,7 @@ module _
           ( id)))
 
   iso-loop-group-fin-UU-Fin-Group :
-    type-iso-Group
+    iso-Group
       ( abstract-group-Concrete-Group (UU-Fin-Group l n))
       ( loop-group-Set (raise-Set l (Fin-Set n)))
   pr1 iso-loop-group-fin-UU-Fin-Group =
diff --git a/src/finite-group-theory/groups-of-order-2.lagda.md b/src/finite-group-theory/groups-of-order-2.lagda.md
index 6d766f606e..5425077ad3 100644
--- a/src/finite-group-theory/groups-of-order-2.lagda.md
+++ b/src/finite-group-theory/groups-of-order-2.lagda.md
@@ -102,7 +102,7 @@ iso-Group-of-Order-2 :
   {l1 l2 : Level} (G : Group-of-Order-2 l1) (H : Group-of-Order-2 l2) →
   UU (l1 ⊔ l2)
 iso-Group-of-Order-2 G H =
-  type-iso-Group (group-Group-of-Order-2 G) (group-Group-of-Order-2 H)
+  iso-Group (group-Group-of-Order-2 G) (group-Group-of-Order-2 H)
 
 module _
   {l : Level} (G : Group-of-Order-2 l)
diff --git a/src/foundation/images-subtypes.lagda.md b/src/foundation/images-subtypes.lagda.md
index 620c7d57ae..188adaa3c9 100644
--- a/src/foundation/images-subtypes.lagda.md
+++ b/src/foundation/images-subtypes.lagda.md
@@ -28,7 +28,7 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
   where
 
-  subtype-im-subtype :
+  im-subtype :
     {l3 : Level} → subtype l3 A → subtype (l1 ⊔ l2 ⊔ l3) B
-  subtype-im-subtype S y = subtype-im (f ∘ inclusion-subtype S) y
+  im-subtype S y = subtype-im (f ∘ inclusion-subtype S) y
 ```
diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md
index 917c06bbea..23cda3371b 100644
--- a/src/group-theory.lagda.md
+++ b/src/group-theory.lagda.md
@@ -25,6 +25,7 @@ open import group-theory.central-elements-groups public
 open import group-theory.central-elements-monoids public
 open import group-theory.central-elements-semigroups public
 open import group-theory.centralizer-subgroups public
+open import group-theory.characteristic-subgroups public
 open import group-theory.commutative-monoids public
 open import group-theory.commutator-subgroups public
 open import group-theory.commutators-of-elements-groups public
diff --git a/src/group-theory/category-of-groups.lagda.md b/src/group-theory/category-of-groups.lagda.md
index 61b96665d3..b2352001ab 100644
--- a/src/group-theory/category-of-groups.lagda.md
+++ b/src/group-theory/category-of-groups.lagda.md
@@ -32,7 +32,7 @@ is-large-category-Group G =
     ( is-contr-total-iso-Group G)
     ( iso-eq-Group G)
 
-eq-iso-Group : {l : Level} (G H : Group l) → type-iso-Group G H → Id G H
+eq-iso-Group : {l : Level} (G H : Group l) → iso-Group G H → Id G H
 eq-iso-Group G H = map-inv-is-equiv (is-large-category-Group G H)
 
 Group-Large-Category : Large-Category lsuc (_⊔_)
diff --git a/src/group-theory/category-of-semigroups.lagda.md b/src/group-theory/category-of-semigroups.lagda.md
index 37c84d0b45..b9f7ea6756 100644
--- a/src/group-theory/category-of-semigroups.lagda.md
+++ b/src/group-theory/category-of-semigroups.lagda.md
@@ -41,12 +41,12 @@ is-large-category-Semigroup G =
     ( iso-eq-Semigroup G)
 
 extensionality-Semigroup :
-  {l : Level} (G H : Semigroup l) → Id G H ≃ type-iso-Semigroup G H
+  {l : Level} (G H : Semigroup l) → Id G H ≃ iso-Semigroup G H
 pr1 (extensionality-Semigroup G H) = iso-eq-Semigroup G H
 pr2 (extensionality-Semigroup G H) = is-large-category-Semigroup G H
 
 eq-iso-Semigroup :
-  {l : Level} (G H : Semigroup l) → type-iso-Semigroup G H → Id G H
+  {l : Level} (G H : Semigroup l) → iso-Semigroup G H → Id G H
 eq-iso-Semigroup G H = map-inv-is-equiv (is-large-category-Semigroup G H)
 
 Semigroup-Large-Category : Large-Category lsuc (_⊔_)
diff --git a/src/group-theory/characteristic-subgroups.lagda.md b/src/group-theory/characteristic-subgroups.lagda.md
new file mode 100644
index 0000000000..1730163d60
--- /dev/null
+++ b/src/group-theory/characteristic-subgroups.lagda.md
@@ -0,0 +1,75 @@
+# Characteristic subgroups
+
+```agda
+module group-theory.characteristic-subgroups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import group-theory.groups
+open import group-theory.images-of-group-homomorphisms
+open import group-theory.isomorphisms-groups
+open import group-theory.subgroups
+```
+
+</details>
+
+## Idea
+
+A **characteristic subgroup** of a [group](group-theory.groups.md) `G` is a
+[subgroup](group-theory.subgroups.md) `H` of `G` such that `f H ⊆ H` for every
+[isomorphism](group-theory.isomorphisms-groups.md) `f : G ≅ G`. The seemingly
+stronger condition, which asserts that `f H ＝ H` for every isomorphism
+`f : G ≅ G` is equivalent.
+
+Note that any characteristic subgroup is
+[normal](group-theory.normal-subgroups.md), since the condition of being
+characteristic implies that `conjugation x H ＝ H`.
+
+## Definition
+
+### The predicate of being a characteristic subgroup
+
+```agda
+module _
+  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G)
+  where
+
+  is-characteristic-prop-Subgroup : Prop (l1 ⊔ l2)
+  is-characteristic-prop-Subgroup =
+    Π-Prop
+      ( iso-Group G G)
+      ( λ f →
+        leq-prop-Subgroup G
+          ( im-hom-Subgroup G G (hom-iso-Group G G f) H)
+          ( H))
+```
+
+### The stronger predicate of being a characteristic subgroup
+
+```agda
+module _
+  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G)
+  where
+
+  is-characteristic-prop-Subgroup' : Prop (l1 ⊔ l2)
+  is-characteristic-prop-Subgroup' =
+    Π-Prop
+      ( iso-Group G G)
+      ( λ f →
+        has-same-elements-prop-Subgroup G
+          ( im-hom-Subgroup G G (hom-iso-Group G G f) H)
+          ( H))
+```
+
+## See also
+
+- [Characteristic subgroup](https://groupprops.subwiki.org/wiki/Characteristic_subgroup)
+  at Groupprops
+- [Characteristic subgroup](https://www.wikidata.org/entity/Q747027) at Wikidata
+- [Characteristic subgroup](https://en.wikipedia.org/wiki/Characteristic_subgroup)
+  at Wikipedia
diff --git a/src/group-theory/conjugation.lagda.md b/src/group-theory/conjugation.lagda.md
index f5e6d396e0..c6a6e28e3b 100644
--- a/src/group-theory/conjugation.lagda.md
+++ b/src/group-theory/conjugation.lagda.md
@@ -385,7 +385,7 @@ module _
   pr1 (conjugation-equiv-Group x) = equiv-conjugation-Group G x
   pr2 (conjugation-equiv-Group x) = distributive-conjugation-mul-Group G x
 
-  conjugation-iso-Group : type-Group G → type-iso-Group G G
+  conjugation-iso-Group : type-Group G → iso-Group G G
   conjugation-iso-Group x = iso-equiv-Group G G (conjugation-equiv-Group x)
 
   preserves-integer-powers-conjugation-Group :
diff --git a/src/group-theory/epimorphisms-groups.lagda.md b/src/group-theory/epimorphisms-groups.lagda.md
index 57ea1a5389..328edec5c1 100644
--- a/src/group-theory/epimorphisms-groups.lagda.md
+++ b/src/group-theory/epimorphisms-groups.lagda.md
@@ -60,7 +60,7 @@ module _
 ```agda
 module _
   {l1 l2 : Level} (l3 : Level) (G : Group l1)
-  (H : Group l2) (f : type-iso-Group G H)
+  (H : Group l2) (f : iso-Group G H)
   where
 
   is-epi-iso-Group :
diff --git a/src/group-theory/full-subgroups.lagda.md b/src/group-theory/full-subgroups.lagda.md
index 5d37b0e097..09f1268b8e 100644
--- a/src/group-theory/full-subgroups.lagda.md
+++ b/src/group-theory/full-subgroups.lagda.md
@@ -111,12 +111,12 @@ module _
   pr2 equiv-group-inclusion-full-Subgroup =
     preserves-mul-inclusion-full-Subgroup
 
-  iso-full-Subgroup : type-iso-Group group-full-Subgroup G
+  iso-full-Subgroup : iso-Group group-full-Subgroup G
   iso-full-Subgroup =
     iso-equiv-Group group-full-Subgroup G equiv-group-inclusion-full-Subgroup
 
   inv-iso-full-Subgroup :
-    type-iso-Group G group-full-Subgroup
+    iso-Group G group-full-Subgroup
   inv-iso-full-Subgroup =
     inv-iso-Group group-full-Subgroup G iso-full-Subgroup
 ```
@@ -141,7 +141,7 @@ module _
       ( is-equiv-inclusion-is-full-subtype (subset-Subgroup G H) K)
 
   iso-inclusion-is-full-Subgroup :
-    is-full-Subgroup G H → type-iso-Group (group-Subgroup G H) G
+    is-full-Subgroup G H → iso-Group (group-Subgroup G H) G
   pr1 (iso-inclusion-is-full-Subgroup K) = hom-inclusion-Subgroup G H
   pr2 (iso-inclusion-is-full-Subgroup K) = is-iso-inclusion-is-full-Subgroup K
 
diff --git a/src/group-theory/generating-elements-groups.lagda.md b/src/group-theory/generating-elements-groups.lagda.md
index a2ed29ade4..404159da0b 100644
--- a/src/group-theory/generating-elements-groups.lagda.md
+++ b/src/group-theory/generating-elements-groups.lagda.md
@@ -607,7 +607,7 @@ module _
       ( is-equiv-ev-element-Group-With-Generating-Element)
 
   iso-ev-element-Group-With-Generating-Element :
-    type-iso-Ab
+    iso-Ab
       ( ab-hom-Ab
         ( abelian-group-Group-With-Generating-Element G)
         ( abelian-group-Group-With-Generating-Element G))
diff --git a/src/group-theory/images-of-group-homomorphisms.lagda.md b/src/group-theory/images-of-group-homomorphisms.lagda.md
index a10218a290..fbc809b7a3 100644
--- a/src/group-theory/images-of-group-homomorphisms.lagda.md
+++ b/src/group-theory/images-of-group-homomorphisms.lagda.md
@@ -10,6 +10,7 @@ module group-theory.images-of-group-homomorphisms where
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.images
+open import foundation.images-subtypes
 open import foundation.logical-equivalences
 open import foundation.propositional-truncations
 open import foundation.universal-property-image
@@ -128,6 +129,58 @@ module _
     backward-implication (is-image-image-hom-Group K)
 ```
 
+### The image of a subgroup of a group homomorphism
+
+```agda
+module _
+  {l1 l2 l3 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
+  (K : Subgroup l3 G)
+  where
+
+  subset-im-hom-Subgroup : subset-Group (l1 ⊔ l2 ⊔ l3) H
+  subset-im-hom-Subgroup =
+    im-subtype (map-hom-Group G H f) (subset-Subgroup G K)
+
+  contains-unit-im-hom-Subgroup :
+    contains-unit-subset-Group H subset-im-hom-Subgroup
+  contains-unit-im-hom-Subgroup =
+    unit-trunc-Prop (unit-Subgroup G K , preserves-unit-hom-Group G H f)
+
+  abstract
+    is-closed-under-multiplication-im-hom-Subgroup :
+      is-closed-under-multiplication-subset-Group H subset-im-hom-Subgroup
+    is-closed-under-multiplication-im-hom-Subgroup x y u v =
+      apply-twice-universal-property-trunc-Prop u v
+        ( subset-im-hom-Subgroup (mul-Group H x y))
+        ( λ where
+          ((x' , k) , refl) ((y' , l) , refl) →
+            unit-trunc-Prop
+              ( ( mul-Subgroup G K (x' , k) (y' , l)) ,
+                ( preserves-mul-hom-Group G H f x' y')))
+
+  abstract
+    is-closed-under-inverses-im-hom-Subgroup :
+      is-closed-under-inverses-subset-Group H subset-im-hom-Subgroup
+    is-closed-under-inverses-im-hom-Subgroup x u =
+      apply-universal-property-trunc-Prop u
+        ( subset-im-hom-Subgroup (inv-Group H x))
+        ( λ where
+          ((x' , k) , refl) →
+            unit-trunc-Prop
+              ( ( inv-Subgroup G K (x' , k)) ,
+                ( preserves-inv-hom-Group G H f x')))
+
+  im-hom-Subgroup : Subgroup (l1 ⊔ l2 ⊔ l3) H
+  pr1 im-hom-Subgroup =
+    subset-im-hom-Subgroup
+  pr1 (pr2 im-hom-Subgroup) =
+    contains-unit-im-hom-Subgroup
+  pr1 (pr2 (pr2 im-hom-Subgroup)) =
+    is-closed-under-multiplication-im-hom-Subgroup
+  pr2 (pr2 (pr2 im-hom-Subgroup)) =
+    is-closed-under-inverses-im-hom-Subgroup
+```
+
 ## Properties
 
 ### A group homomorphism is surjective if and only if its image is the full subgroup
diff --git a/src/group-theory/isomorphisms-abelian-groups.lagda.md b/src/group-theory/isomorphisms-abelian-groups.lagda.md
index c9cb16f0ff..ebcb01fab1 100644
--- a/src/group-theory/isomorphisms-abelian-groups.lagda.md
+++ b/src/group-theory/isomorphisms-abelian-groups.lagda.md
@@ -110,56 +110,56 @@ module _
   {l1 l2 : Level} (A : Ab l1) (B : Ab l2)
   where
 
-  type-iso-Ab : UU (l1 ⊔ l2)
-  type-iso-Ab = type-iso-Group (group-Ab A) (group-Ab B)
+  iso-Ab : UU (l1 ⊔ l2)
+  iso-Ab = iso-Group (group-Ab A) (group-Ab B)
 
-  hom-iso-Ab : type-iso-Ab → hom-Ab A B
+  hom-iso-Ab : iso-Ab → hom-Ab A B
   hom-iso-Ab = hom-iso-Group (group-Ab A) (group-Ab B)
 
-  map-iso-Ab : type-iso-Ab → type-Ab A → type-Ab B
+  map-iso-Ab : iso-Ab → type-Ab A → type-Ab B
   map-iso-Ab = map-iso-Group (group-Ab A) (group-Ab B)
 
   preserves-add-iso-Ab :
-    (f : type-iso-Ab) (x y : type-Ab A) →
+    (f : iso-Ab) (x y : type-Ab A) →
     map-iso-Ab f (add-Ab A x y) ＝ add-Ab B (map-iso-Ab f x) (map-iso-Ab f y)
   preserves-add-iso-Ab =
     preserves-mul-iso-Group (group-Ab A) (group-Ab B)
 
-  is-iso-iso-Ab : (f : type-iso-Ab) → is-iso-Ab A B (hom-iso-Ab f)
+  is-iso-iso-Ab : (f : iso-Ab) → is-iso-Ab A B (hom-iso-Ab f)
   is-iso-iso-Ab = is-iso-iso-Group (group-Ab A) (group-Ab B)
 
-  hom-inv-iso-Ab : type-iso-Ab → hom-Ab B A
+  hom-inv-iso-Ab : iso-Ab → hom-Ab B A
   hom-inv-iso-Ab = hom-inv-iso-Group (group-Ab A) (group-Ab B)
 
-  map-inv-iso-Ab : type-iso-Ab → type-Ab B → type-Ab A
+  map-inv-iso-Ab : iso-Ab → type-Ab B → type-Ab A
   map-inv-iso-Ab = map-inv-iso-Group (group-Ab A) (group-Ab B)
 
   preserves-add-inv-iso-Ab :
-    (f : type-iso-Ab) (x y : type-Ab B) →
+    (f : iso-Ab) (x y : type-Ab B) →
     map-inv-iso-Ab f (add-Ab B x y) ＝
     add-Ab A (map-inv-iso-Ab f x) (map-inv-iso-Ab f y)
   preserves-add-inv-iso-Ab =
     preserves-mul-inv-iso-Group (group-Ab A) (group-Ab B)
 
   is-section-hom-inv-iso-Ab :
-    (f : type-iso-Ab) →
+    (f : iso-Ab) →
     comp-hom-Ab B A B (hom-iso-Ab f) (hom-inv-iso-Ab f) ＝ id-hom-Ab B
   is-section-hom-inv-iso-Ab =
     is-section-hom-inv-iso-Group (group-Ab A) (group-Ab B)
 
   is-section-map-inv-iso-Ab :
-    (f : type-iso-Ab) → (map-iso-Ab f ∘ map-inv-iso-Ab f) ~ id
+    (f : iso-Ab) → (map-iso-Ab f ∘ map-inv-iso-Ab f) ~ id
   is-section-map-inv-iso-Ab =
     is-section-map-inv-iso-Group (group-Ab A) (group-Ab B)
 
   is-retraction-hom-inv-iso-Ab :
-    (f : type-iso-Ab) →
+    (f : iso-Ab) →
     comp-hom-Ab A B A (hom-inv-iso-Ab f) (hom-iso-Ab f) ＝ id-hom-Ab A
   is-retraction-hom-inv-iso-Ab =
     is-retraction-hom-inv-iso-Group (group-Ab A) (group-Ab B)
 
   is-retraction-map-inv-iso-Ab :
-    (f : type-iso-Ab) → (map-inv-iso-Ab f ∘ map-iso-Ab f) ~ id
+    (f : iso-Ab) → (map-inv-iso-Ab f ∘ map-iso-Ab f) ~ id
   is-retraction-map-inv-iso-Ab =
     is-retraction-map-inv-iso-Group (group-Ab A) (group-Ab B)
 ```
@@ -168,7 +168,7 @@ module _
 
 ```agda
 id-iso-Ab :
-  {l : Level} (A : Ab l) → type-iso-Ab A A
+  {l : Level} (A : Ab l) → iso-Ab A A
 id-iso-Ab A = id-iso-Group (group-Ab A)
 ```
 
@@ -178,19 +178,19 @@ id-iso-Ab A = id-iso-Group (group-Ab A)
 
 ```agda
 iso-eq-Ab :
-  {l : Level} (A B : Ab l) → Id A B → type-iso-Ab A B
+  {l : Level} (A B : Ab l) → Id A B → iso-Ab A B
 iso-eq-Ab A .A refl = id-iso-Ab A
 
 abstract
   equiv-iso-eq-Ab' :
-    {l : Level} (A B : Ab l) → Id A B ≃ type-iso-Ab A B
+    {l : Level} (A B : Ab l) → Id A B ≃ iso-Ab A B
   equiv-iso-eq-Ab' A B =
     ( extensionality-Group' (group-Ab A) (group-Ab B)) ∘e
     ( equiv-ap-inclusion-subtype is-abelian-group-Prop {A} {B})
 
 abstract
   is-contr-total-iso-Ab :
-    {l : Level} (A : Ab l) → is-contr (Σ (Ab l) (type-iso-Ab A))
+    {l : Level} (A : Ab l) → is-contr (Σ (Ab l) (iso-Ab A))
   is-contr-total-iso-Ab {l} A =
     is-contr-equiv'
       ( Σ (Ab l) (Id A))
@@ -205,7 +205,7 @@ is-equiv-iso-eq-Ab A =
     ( iso-eq-Ab A)
 
 eq-iso-Ab :
-  {l : Level} (A B : Ab l) → type-iso-Ab A B → Id A B
+  {l : Level} (A B : Ab l) → iso-Ab A B → Id A B
 eq-iso-Ab A B = map-inv-is-equiv (is-equiv-iso-eq-Ab A B)
 ```
 
@@ -224,9 +224,9 @@ module _
     (f : hom-Ab A B) → is-iso-Ab A B f → is-equiv-hom-Ab A B f
   is-equiv-is-iso-Ab = is-equiv-is-iso-Group (group-Ab A) (group-Ab B)
 
-  equiv-iso-equiv-Ab : equiv-Ab A B ≃ type-iso-Ab A B
+  equiv-iso-equiv-Ab : equiv-Ab A B ≃ iso-Ab A B
   equiv-iso-equiv-Ab = equiv-iso-equiv-Group (group-Ab A) (group-Ab B)
 
-  iso-equiv-Ab : equiv-Ab A B → type-iso-Ab A B
+  iso-equiv-Ab : equiv-Ab A B → iso-Ab A B
   iso-equiv-Ab = iso-equiv-Group (group-Ab A) (group-Ab B)
 ```
diff --git a/src/group-theory/isomorphisms-group-actions.lagda.md b/src/group-theory/isomorphisms-group-actions.lagda.md
index 6348da769b..c91df924be 100644
--- a/src/group-theory/isomorphisms-group-actions.lagda.md
+++ b/src/group-theory/isomorphisms-group-actions.lagda.md
@@ -40,21 +40,21 @@ module _
   is-iso-Abstract-Group-Action =
     is-iso-Large-Precategory C {X = X} {Y = Y}
 
-  type-iso-Abstract-Group-Action : UU (l1 ⊔ l2 ⊔ l3)
-  type-iso-Abstract-Group-Action = iso-Large-Precategory C X Y
+  iso-Abstract-Group-Action : UU (l1 ⊔ l2 ⊔ l3)
+  iso-Abstract-Group-Action = iso-Large-Precategory C X Y
 
   hom-iso-Abstract-Group-Action :
-    type-iso-Abstract-Group-Action → hom-Abstract-Group-Action G X Y
+    iso-Abstract-Group-Action → hom-Abstract-Group-Action G X Y
   hom-iso-Abstract-Group-Action = hom-iso-Large-Precategory C {X = X} {Y = Y}
 
   map-iso-Abstract-Group-Action :
-    type-iso-Abstract-Group-Action →
+    iso-Abstract-Group-Action →
     type-Abstract-Group-Action G X → type-Abstract-Group-Action G Y
   map-iso-Abstract-Group-Action f =
     map-hom-Abstract-Group-Action G X Y (hom-iso-Abstract-Group-Action f)
 
   coherence-square-iso-Abstract-Group-Action :
-    (f : type-iso-Abstract-Group-Action) (g : type-Group G) →
+    (f : iso-Abstract-Group-Action) (g : type-Group G) →
     coherence-square-maps
       ( map-iso-Abstract-Group-Action f)
       ( mul-Abstract-Group-Action G X g)
@@ -65,19 +65,19 @@ module _
       ( hom-iso-Abstract-Group-Action f)
 
   hom-inv-iso-Abstract-Group-Action :
-    type-iso-Abstract-Group-Action → hom-Abstract-Group-Action G Y X
+    iso-Abstract-Group-Action → hom-Abstract-Group-Action G Y X
   hom-inv-iso-Abstract-Group-Action =
     hom-inv-iso-Large-Precategory C {X = X} {Y = Y}
 
   map-hom-inv-iso-Abstract-Group-Action :
-    type-iso-Abstract-Group-Action →
+    iso-Abstract-Group-Action →
     type-Abstract-Group-Action G Y → type-Abstract-Group-Action G X
   map-hom-inv-iso-Abstract-Group-Action f =
     map-hom-Abstract-Group-Action G Y X
       ( hom-inv-iso-Abstract-Group-Action f)
 
   is-section-hom-inv-iso-Abstract-Group-Action :
-    (f : type-iso-Abstract-Group-Action) →
+    (f : iso-Abstract-Group-Action) →
     Id
       ( comp-hom-Abstract-Group-Action G Y X Y
         ( hom-iso-Abstract-Group-Action f)
@@ -87,7 +87,7 @@ module _
     is-section-hom-inv-iso-Large-Precategory C {X = X} {Y = Y}
 
   is-retraction-hom-inv-iso-Abstract-Group-Action :
-    (f : type-iso-Abstract-Group-Action) →
+    (f : iso-Abstract-Group-Action) →
     Id
       ( comp-hom-Abstract-Group-Action G X Y X
         ( hom-inv-iso-Abstract-Group-Action f)
@@ -97,13 +97,13 @@ module _
     is-retraction-hom-inv-iso-Large-Precategory C {X = X} {Y = Y}
 
   is-iso-iso-Abstract-Group-Action :
-    (f : type-iso-Abstract-Group-Action) →
+    (f : iso-Abstract-Group-Action) →
     is-iso-Abstract-Group-Action (hom-iso-Abstract-Group-Action f)
   is-iso-iso-Abstract-Group-Action =
     is-iso-iso-Large-Precategory C {X = X} {Y = Y}
 
   equiv-iso-Abstract-Group-Action :
-    type-iso-Abstract-Group-Action → equiv-Abstract-Group-Action G X Y
+    iso-Abstract-Group-Action → equiv-Abstract-Group-Action G X Y
   pr1 (pr1 (equiv-iso-Abstract-Group-Action f)) =
     map-iso-Abstract-Group-Action f
   pr2 (pr1 (equiv-iso-Abstract-Group-Action f)) =
diff --git a/src/group-theory/isomorphisms-groups.lagda.md b/src/group-theory/isomorphisms-groups.lagda.md
index 5a3a7e7496..00a4a30abb 100644
--- a/src/group-theory/isomorphisms-groups.lagda.md
+++ b/src/group-theory/isomorphisms-groups.lagda.md
@@ -122,57 +122,57 @@ module _
   {l1 l2 : Level} (G : Group l1) (H : Group l2)
   where
 
-  type-iso-Group : UU (l1 ⊔ l2)
-  type-iso-Group = type-iso-Semigroup (semigroup-Group G) (semigroup-Group H)
+  iso-Group : UU (l1 ⊔ l2)
+  iso-Group = iso-Semigroup (semigroup-Group G) (semigroup-Group H)
 
-  hom-iso-Group : type-iso-Group → hom-Group G H
+  hom-iso-Group : iso-Group → hom-Group G H
   hom-iso-Group = hom-iso-Semigroup (semigroup-Group G) (semigroup-Group H)
 
-  map-iso-Group : type-iso-Group → type-Group G → type-Group H
+  map-iso-Group : iso-Group → type-Group G → type-Group H
   map-iso-Group = map-iso-Semigroup (semigroup-Group G) (semigroup-Group H)
 
   preserves-mul-iso-Group :
-    (f : type-iso-Group) (x y : type-Group G) →
+    (f : iso-Group) (x y : type-Group G) →
     map-iso-Group f (mul-Group G x y) ＝
     mul-Group H (map-iso-Group f x) (map-iso-Group f y)
   preserves-mul-iso-Group =
     preserves-mul-iso-Semigroup (semigroup-Group G) (semigroup-Group H)
 
   is-iso-iso-Group :
-    (f : type-iso-Group) → is-iso-Group G H (hom-iso-Group f)
+    (f : iso-Group) → is-iso-Group G H (hom-iso-Group f)
   is-iso-iso-Group =
     is-iso-iso-Semigroup (semigroup-Group G) (semigroup-Group H)
 
-  hom-inv-iso-Group : type-iso-Group → hom-Group H G
+  hom-inv-iso-Group : iso-Group → hom-Group H G
   hom-inv-iso-Group =
     hom-inv-iso-Semigroup (semigroup-Group G) (semigroup-Group H)
 
-  map-inv-iso-Group : type-iso-Group → type-Group H → type-Group G
+  map-inv-iso-Group : iso-Group → type-Group H → type-Group G
   map-inv-iso-Group =
     map-inv-iso-Semigroup (semigroup-Group G) (semigroup-Group H)
 
   preserves-mul-inv-iso-Group :
-    (f : type-iso-Group) (x y : type-Group H) →
+    (f : iso-Group) (x y : type-Group H) →
     map-inv-iso-Group f (mul-Group H x y) ＝
     mul-Group G (map-inv-iso-Group f x) (map-inv-iso-Group f y)
   preserves-mul-inv-iso-Group =
     preserves-mul-inv-iso-Semigroup (semigroup-Group G) (semigroup-Group H)
 
   is-section-hom-inv-iso-Group :
-    (f : type-iso-Group) →
+    (f : iso-Group) →
     comp-hom-Group H G H (hom-iso-Group f) (hom-inv-iso-Group f) ＝
     id-hom-Group H
   is-section-hom-inv-iso-Group =
     is-section-hom-inv-iso-Semigroup (semigroup-Group G) (semigroup-Group H)
 
   is-section-map-inv-iso-Group :
-    (f : type-iso-Group) →
+    (f : iso-Group) →
     ( map-iso-Group f ∘ map-inv-iso-Group f) ~ id
   is-section-map-inv-iso-Group =
     is-section-map-inv-iso-Semigroup (semigroup-Group G) (semigroup-Group H)
 
   is-retraction-hom-inv-iso-Group :
-    (f : type-iso-Group) →
+    (f : iso-Group) →
     comp-hom-Group G H G (hom-inv-iso-Group f) (hom-iso-Group f) ＝
     id-hom-Group G
   is-retraction-hom-inv-iso-Group =
@@ -181,7 +181,7 @@ module _
       ( semigroup-Group H)
 
   is-retraction-map-inv-iso-Group :
-    (f : type-iso-Group) →
+    (f : iso-Group) →
     ( map-inv-iso-Group f ∘ map-iso-Group f) ~ id
   is-retraction-map-inv-iso-Group =
     is-retraction-map-inv-iso-Semigroup
@@ -198,11 +198,11 @@ module _
   is-equiv-is-iso-Group =
     is-equiv-is-iso-Semigroup (semigroup-Group G) (semigroup-Group H)
 
-  equiv-iso-equiv-Group : equiv-Group G H ≃ type-iso-Group
+  equiv-iso-equiv-Group : equiv-Group G H ≃ iso-Group
   equiv-iso-equiv-Group =
     equiv-iso-equiv-Semigroup (semigroup-Group G) (semigroup-Group H)
 
-  iso-equiv-Group : equiv-Group G H → type-iso-Group
+  iso-equiv-Group : equiv-Group G H → iso-Group
   iso-equiv-Group = map-equiv equiv-iso-equiv-Group
 ```
 
@@ -213,7 +213,7 @@ module _
   {l : Level} (G : Group l)
   where
 
-  id-iso-Group : type-iso-Group G G
+  id-iso-Group : iso-Group G G
   id-iso-Group = id-iso-Large-Precategory Group-Large-Precategory {X = G}
 ```
 
@@ -226,11 +226,11 @@ module _
   {l : Level} (G : Group l)
   where
 
-  iso-eq-Group : (H : Group l) → Id G H → type-iso-Group G H
+  iso-eq-Group : (H : Group l) → Id G H → iso-Group G H
   iso-eq-Group = iso-eq-Large-Precategory Group-Large-Precategory G
 
   abstract
-    extensionality-Group' : (H : Group l) → Id G H ≃ type-iso-Group G H
+    extensionality-Group' : (H : Group l) → Id G H ≃ iso-Group G H
     extensionality-Group' H =
       ( extensionality-Semigroup
         ( semigroup-Group G)
@@ -238,7 +238,7 @@ module _
       ( equiv-ap-inclusion-subtype is-group-Prop {s = G} {t = H})
 
   abstract
-    is-contr-total-iso-Group : is-contr (Σ (Group l) (type-iso-Group G))
+    is-contr-total-iso-Group : is-contr (Σ (Group l) (iso-Group G))
     is-contr-total-iso-Group =
       is-contr-equiv'
         ( Σ (Group l) (Id G))
@@ -254,7 +254,7 @@ module _
   where
 
   comp-iso-Group :
-    type-iso-Group H K → type-iso-Group G H → type-iso-Group G K
+    iso-Group H K → iso-Group G H → iso-Group G K
   comp-iso-Group =
     comp-iso-Large-Precategory Group-Large-Precategory {X = G} {Y = H} {Z = K}
 ```
@@ -266,7 +266,7 @@ module _
   {l1 l2 : Level} (G : Group l1) (H : Group l2)
   where
 
-  inv-iso-Group : type-iso-Group G H → type-iso-Group H G
+  inv-iso-Group : iso-Group G H → iso-Group H G
   inv-iso-Group =
     inv-iso-Large-Precategory Group-Large-Precategory {X = G} {Y = H}
 ```
diff --git a/src/group-theory/isomorphisms-semigroups.lagda.md b/src/group-theory/isomorphisms-semigroups.lagda.md
index 2192522f6d..fc84c6d66a 100644
--- a/src/group-theory/isomorphisms-semigroups.lagda.md
+++ b/src/group-theory/isomorphisms-semigroups.lagda.md
@@ -112,46 +112,46 @@ module _
   {l1 l2 : Level} (G : Semigroup l1) (H : Semigroup l2)
   where
 
-  type-iso-Semigroup : UU (l1 ⊔ l2)
-  type-iso-Semigroup = iso-Large-Precategory Semigroup-Large-Precategory G H
+  iso-Semigroup : UU (l1 ⊔ l2)
+  iso-Semigroup = iso-Large-Precategory Semigroup-Large-Precategory G H
 
-  hom-iso-Semigroup : type-iso-Semigroup → hom-Semigroup G H
+  hom-iso-Semigroup : iso-Semigroup → hom-Semigroup G H
   hom-iso-Semigroup =
     hom-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H}
 
-  map-iso-Semigroup : type-iso-Semigroup → type-Semigroup G → type-Semigroup H
+  map-iso-Semigroup : iso-Semigroup → type-Semigroup G → type-Semigroup H
   map-iso-Semigroup f = map-hom-Semigroup G H (hom-iso-Semigroup f)
 
   preserves-mul-iso-Semigroup :
-    (f : type-iso-Semigroup) (x y : type-Semigroup G) →
+    (f : iso-Semigroup) (x y : type-Semigroup G) →
     map-iso-Semigroup f (mul-Semigroup G x y) ＝
     mul-Semigroup H (map-iso-Semigroup f x) (map-iso-Semigroup f y)
   preserves-mul-iso-Semigroup f =
     preserves-mul-hom-Semigroup G H (hom-iso-Semigroup f)
 
   is-iso-iso-Semigroup :
-    (f : type-iso-Semigroup) → is-iso-Semigroup G H (hom-iso-Semigroup f)
+    (f : iso-Semigroup) → is-iso-Semigroup G H (hom-iso-Semigroup f)
   is-iso-iso-Semigroup =
     is-iso-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H}
 
-  hom-inv-iso-Semigroup : type-iso-Semigroup → hom-Semigroup H G
+  hom-inv-iso-Semigroup : iso-Semigroup → hom-Semigroup H G
   hom-inv-iso-Semigroup =
     hom-inv-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H}
 
   map-inv-iso-Semigroup :
-    type-iso-Semigroup → type-Semigroup H → type-Semigroup G
+    iso-Semigroup → type-Semigroup H → type-Semigroup G
   map-inv-iso-Semigroup f =
     map-hom-Semigroup H G (hom-inv-iso-Semigroup f)
 
   preserves-mul-inv-iso-Semigroup :
-    (f : type-iso-Semigroup) (x y : type-Semigroup H) →
+    (f : iso-Semigroup) (x y : type-Semigroup H) →
     map-inv-iso-Semigroup f (mul-Semigroup H x y) ＝
     mul-Semigroup G (map-inv-iso-Semigroup f x) (map-inv-iso-Semigroup f y)
   preserves-mul-inv-iso-Semigroup f =
     preserves-mul-hom-Semigroup H G (hom-inv-iso-Semigroup f)
 
   is-section-hom-inv-iso-Semigroup :
-    (f : type-iso-Semigroup) →
+    (f : iso-Semigroup) →
     comp-hom-Semigroup H G H (hom-iso-Semigroup f) (hom-inv-iso-Semigroup f) ＝
     id-hom-Semigroup H
   is-section-hom-inv-iso-Semigroup =
@@ -161,7 +161,7 @@ module _
       { Y = H}
 
   is-section-map-inv-iso-Semigroup :
-    (f : type-iso-Semigroup) →
+    (f : iso-Semigroup) →
     (map-iso-Semigroup f ∘ map-inv-iso-Semigroup f) ~ id
   is-section-map-inv-iso-Semigroup f =
     htpy-eq-hom-Semigroup H H
@@ -172,7 +172,7 @@ module _
       ( is-section-hom-inv-iso-Semigroup f)
 
   is-retraction-hom-inv-iso-Semigroup :
-    (f : type-iso-Semigroup) →
+    (f : iso-Semigroup) →
     comp-hom-Semigroup G H G (hom-inv-iso-Semigroup f) (hom-iso-Semigroup f) ＝
     id-hom-Semigroup G
   is-retraction-hom-inv-iso-Semigroup =
@@ -182,7 +182,7 @@ module _
       { Y = H}
 
   is-retraction-map-inv-iso-Semigroup :
-    (f : type-iso-Semigroup) →
+    (f : iso-Semigroup) →
     ( map-inv-iso-Semigroup f ∘ map-iso-Semigroup f) ~ id
   is-retraction-map-inv-iso-Semigroup f =
     htpy-eq-hom-Semigroup G G
@@ -281,7 +281,7 @@ module _
         ( htpy-eq (ap pr1 S))
         ( htpy-eq (ap pr1 R))
 
-  equiv-iso-equiv-Semigroup : equiv-Semigroup G H ≃ type-iso-Semigroup G H
+  equiv-iso-equiv-Semigroup : equiv-Semigroup G H ≃ iso-Semigroup G H
   equiv-iso-equiv-Semigroup =
     ( equiv-type-subtype
       ( λ f → is-property-is-equiv (map-hom-Semigroup G H f))
@@ -299,17 +299,17 @@ module _
   where
 
   is-contr-total-iso-Semigroup :
-    is-contr (Σ (Semigroup l) (type-iso-Semigroup G))
+    is-contr (Σ (Semigroup l) (iso-Semigroup G))
   is-contr-total-iso-Semigroup =
     is-contr-equiv'
       ( Σ (Semigroup l) (equiv-Semigroup G))
       ( equiv-tot (equiv-iso-equiv-Semigroup G))
       ( is-contr-total-equiv-Semigroup G)
 
-  id-iso-Semigroup : type-iso-Semigroup G G
+  id-iso-Semigroup : iso-Semigroup G G
   id-iso-Semigroup =
     id-iso-Large-Precategory Semigroup-Large-Precategory {X = G}
 
-  iso-eq-Semigroup : (H : Semigroup l) → Id G H → type-iso-Semigroup G H
+  iso-eq-Semigroup : (H : Semigroup l) → Id G H → iso-Semigroup G H
   iso-eq-Semigroup = iso-eq-Large-Precategory Semigroup-Large-Precategory G
 ```
diff --git a/src/group-theory/loop-groups-sets.lagda.md b/src/group-theory/loop-groups-sets.lagda.md
index 974547155f..9273085a5e 100644
--- a/src/group-theory/loop-groups-sets.lagda.md
+++ b/src/group-theory/loop-groups-sets.lagda.md
@@ -185,7 +185,7 @@ module _
           ( id)))
 
   iso-symmetric-group-loop-group-Set :
-    type-iso-Group (loop-group-Set X) (symmetric-Group X)
+    iso-Group (loop-group-Set X) (symmetric-Group X)
   pr1 iso-symmetric-group-loop-group-Set = hom-symmetric-group-loop-group-Set
   pr1 (pr2 iso-symmetric-group-loop-group-Set) =
     hom-inv-symmetric-group-loop-group-Set
@@ -325,7 +325,7 @@ module _
           ( id)))
 
   iso-abstract-automorphism-group-loop-group-Set :
-    type-iso-Group
+    iso-Group
       ( loop-group-Set X)
       ( abstract-group-Concrete-Group
         ( Automorphism-Group (Set-1-Type l) X))
@@ -347,7 +347,7 @@ module _
   where
 
   iso-loop-group-equiv-Set :
-    type-iso-Group
+    iso-Group
       ( loop-group-Set X)
       ( loop-group-Set Y)
   iso-loop-group-equiv-Set =
diff --git a/src/group-theory/monomorphisms-groups.lagda.md b/src/group-theory/monomorphisms-groups.lagda.md
index c7eb63ce43..3a7fdfb7fe 100644
--- a/src/group-theory/monomorphisms-groups.lagda.md
+++ b/src/group-theory/monomorphisms-groups.lagda.md
@@ -53,7 +53,7 @@ module _
 ```agda
 module _
   {l1 l2 : Level} (l3 : Level) (G : Group l1)
-  (H : Group l2) (f : type-iso-Group G H)
+  (H : Group l2) (f : iso-Group G H)
   where
 
   is-mono-iso-Group :
diff --git a/src/group-theory/opposite-groups.lagda.md b/src/group-theory/opposite-groups.lagda.md
index 405a000dc9..0acbf3b60b 100644
--- a/src/group-theory/opposite-groups.lagda.md
+++ b/src/group-theory/opposite-groups.lagda.md
@@ -50,6 +50,6 @@ module _
   pr1 equiv-inv-Group = equiv-equiv-inv-Group G
   pr2 equiv-inv-Group = distributive-inv-mul-Group G
 
-  iso-inv-Group : type-iso-Group G (op-Group G)
+  iso-inv-Group : iso-Group G (op-Group G)
   iso-inv-Group = iso-equiv-Group G (op-Group G) equiv-inv-Group
 ```
diff --git a/src/group-theory/symmetric-groups.lagda.md b/src/group-theory/symmetric-groups.lagda.md
index 121b6e2614..62c371ed47 100644
--- a/src/group-theory/symmetric-groups.lagda.md
+++ b/src/group-theory/symmetric-groups.lagda.md
@@ -149,7 +149,7 @@ module _
           ( id)))
 
   iso-symmetric-group-equiv-Set :
-    type-iso-Group (symmetric-Group X) (symmetric-Group Y)
+    iso-Group (symmetric-Group X) (symmetric-Group Y)
   pr1 iso-symmetric-group-equiv-Set = hom-symmetric-group-equiv-Set
   pr1 (pr2 iso-symmetric-group-equiv-Set) = hom-inv-symmetric-group-equiv-Set
   pr1 (pr2 (pr2 iso-symmetric-group-equiv-Set)) =
@@ -200,7 +200,7 @@ module _
     preserves-mul-compute-symmetric-Concrete-Group
 
   compute-symmetric-Concrete-Group' :
-    type-iso-Group
+    iso-Group
       ( op-abstract-group-Concrete-Group (symmetric-Concrete-Group A))
       ( symmetric-Group A)
   compute-symmetric-Concrete-Group' =
@@ -210,7 +210,7 @@ module _
       ( equiv-group-compute-symmetric-Concrete-Group)
 
   compute-symmetric-Concrete-Group :
-    type-iso-Group
+    iso-Group
       ( abstract-group-Concrete-Group (symmetric-Concrete-Group A))
       ( symmetric-Group A)
   compute-symmetric-Concrete-Group =
diff --git a/src/group-theory/torsors.lagda.md b/src/group-theory/torsors.lagda.md
index 2ff40ef901..abff902167 100644
--- a/src/group-theory/torsors.lagda.md
+++ b/src/group-theory/torsors.lagda.md
@@ -666,7 +666,7 @@ module _
     is-0-connected-classifying-type-Concrete-Group concrete-group-Group
 
   abstract-group-concrete-group-Group :
-    type-iso-Group (abstract-group-Concrete-Group concrete-group-Group) G
+    iso-Group (abstract-group-Concrete-Group concrete-group-Group) G
   abstract-group-concrete-group-Group =
     iso-equiv-Group
       ( abstract-group-Concrete-Group concrete-group-Group)
diff --git a/src/order-theory/meet-semilattices.lagda.md b/src/order-theory/meet-semilattices.lagda.md
index 5181ad2c8c..11b6daf8df 100644
--- a/src/order-theory/meet-semilattices.lagda.md
+++ b/src/order-theory/meet-semilattices.lagda.md
@@ -636,7 +636,7 @@ module _
   compute-meet-order-theoretic-meet-semilattice-Meet-Semilattice x y = refl
 
   compute-order-theoretic-meet-semilattice-Meet-Semilattice :
-    type-iso-Semigroup
+    iso-Semigroup
       ( semigroup-Meet-Semilattice A)
       ( semigroup-Meet-Semilattice
         ( meet-semilattice-Order-Theoretic-Meet-Semilattice
diff --git a/src/ring-theory/isomorphisms-rings.lagda.md b/src/ring-theory/isomorphisms-rings.lagda.md
index a112e50e78..ab952ad44c 100644
--- a/src/ring-theory/isomorphisms-rings.lagda.md
+++ b/src/ring-theory/isomorphisms-rings.lagda.md
@@ -302,13 +302,13 @@ module _
 
   iso-ab-Ring : UU (l1 ⊔ l2)
   iso-ab-Ring =
-    Σ ( type-iso-Ab (ab-Ring R) (ab-Ring S))
+    Σ ( iso-Ab (ab-Ring R) (ab-Ring S))
       ( λ f →
         is-ring-homomorphism-hom-Ab R S
           ( hom-iso-Ab (ab-Ring R) (ab-Ring S) f))
 
   iso-ab-iso-ab-Ring :
-    iso-ab-Ring → type-iso-Ab (ab-Ring R) (ab-Ring S)
+    iso-ab-Ring → iso-Ab (ab-Ring R) (ab-Ring S)
   iso-ab-iso-ab-Ring = pr1
 
   is-iso-ab-hom-Ring : hom-Ring R S → UU (l1 ⊔ l2)
@@ -434,7 +434,7 @@ module _
             ( U)))
 
   iso-ab-iso-Ring :
-    iso-Ring R S → type-iso-Ab (ab-Ring R) (ab-Ring S)
+    iso-Ring R S → iso-Ab (ab-Ring R) (ab-Ring S)
   pr1 (iso-ab-iso-Ring f) = hom-ab-hom-Ring R S (hom-iso-Ring R S f)
   pr2 (iso-ab-iso-Ring f) =
     is-iso-ab-is-iso-Ring
diff --git a/src/ring-theory/transporting-ring-structure-along-isomorphisms-abelian-groups.lagda.md b/src/ring-theory/transporting-ring-structure-along-isomorphisms-abelian-groups.lagda.md
index e43661146d..cd604d680c 100644
--- a/src/ring-theory/transporting-ring-structure-along-isomorphisms-abelian-groups.lagda.md
+++ b/src/ring-theory/transporting-ring-structure-along-isomorphisms-abelian-groups.lagda.md
@@ -46,7 +46,7 @@ transported ring structure.
 ```agda
 module _
   {l1 l2 : Level} (R : Ring l1) (A : Ab l2)
-  (f : type-iso-Ab (ab-Ring R) A)
+  (f : iso-Ab (ab-Ring R) A)
   where
 
   one-transport-ring-structure-iso-Ab : type-Ab A
diff --git a/src/univalent-combinatorics/cyclic-finite-types.lagda.md b/src/univalent-combinatorics/cyclic-finite-types.lagda.md
index be72510489..04832db1f7 100644
--- a/src/univalent-combinatorics/cyclic-finite-types.lagda.md
+++ b/src/univalent-combinatorics/cyclic-finite-types.lagda.md
@@ -608,7 +608,7 @@ pr2 (equiv-Ω-Cyclic-Type-Group k) =
   preserves-concat-equiv-compute-Ω-Cyclic-Type k
 
 iso-Ω-Cyclic-Type-Group :
-  (k : ℕ) → type-iso-Group (Ω-Cyclic-Type-Group k) (ℤ-Mod-Group k)
+  (k : ℕ) → iso-Group (Ω-Cyclic-Type-Group k) (ℤ-Mod-Group k)
 iso-Ω-Cyclic-Type-Group k =
   iso-equiv-Group
     ( Ω-Cyclic-Type-Group k)