diff --git a/src/category-theory/functors-large-categories.lagda.md b/src/category-theory/functors-large-categories.lagda.md
index eda64ca996..446bc3c40e 100644
--- a/src/category-theory/functors-large-categories.lagda.md
+++ b/src/category-theory/functors-large-categories.lagda.md
@@ -95,7 +95,7 @@ There is an identity functor on any large category.
 id-functor-Large-Category :
   {αC : Level → Level} {βC : Level → Level → Level} →
   (C : Large-Category αC βC) →
-  functor-Large-Category id C C
+  functor-Large-Category (λ l → l) C C
 id-functor-Large-Category C =
   id-functor-Large-Precategory (large-precategory-Large-Category C)
 ```
diff --git a/src/category-theory/functors-large-precategories.lagda.md b/src/category-theory/functors-large-precategories.lagda.md
index ced47bee15..0c4d15795a 100644
--- a/src/category-theory/functors-large-precategories.lagda.md
+++ b/src/category-theory/functors-large-precategories.lagda.md
@@ -78,7 +78,7 @@ module _
 id-functor-Large-Precategory :
   {αC : Level → Level} {βC : Level → Level → Level} →
   (C : Large-Precategory αC βC) →
-  functor-Large-Precategory id C C
+  functor-Large-Precategory (λ l → l) C C
 obj-functor-Large-Precategory
   ( id-functor-Large-Precategory C) =
   id
@@ -152,7 +152,7 @@ module _
     ( preserves-id-functor-Large-Precategory G)
 
   comp-functor-Large-Precategory :
-    functor-Large-Precategory (γG ∘ γF) C E
+    functor-Large-Precategory (λ l → γG (γF l)) C E
   obj-functor-Large-Precategory
     comp-functor-Large-Precategory =
     obj-comp-functor-Large-Precategory
diff --git a/src/commutative-algebra/groups-of-units-commutative-rings.lagda.md b/src/commutative-algebra/groups-of-units-commutative-rings.lagda.md
index 78637d596c..c0959f4d87 100644
--- a/src/commutative-algebra/groups-of-units-commutative-rings.lagda.md
+++ b/src/commutative-algebra/groups-of-units-commutative-rings.lagda.md
@@ -307,7 +307,7 @@ module _
 
 ```agda
 group-of-units-commutative-ring-functor-Large-Precategory :
-  functor-Large-Precategory id
+  functor-Large-Precategory (λ l → l)
     ( Commutative-Ring-Large-Precategory)
     ( Ab-Large-Precategory)
 obj-functor-Large-Precategory
diff --git a/src/commutative-algebra/poset-of-radical-ideals-commutative-rings.lagda.md b/src/commutative-algebra/poset-of-radical-ideals-commutative-rings.lagda.md
index 974e3b3e61..462aa0a5f4 100644
--- a/src/commutative-algebra/poset-of-radical-ideals-commutative-rings.lagda.md
+++ b/src/commutative-algebra/poset-of-radical-ideals-commutative-rings.lagda.md
@@ -180,7 +180,8 @@ module _
   preserves-order-ideal-radical-ideal-Commutative-Ring I J H = H
 
   ideal-radical-ideal-hom-large-poset-Commutative-Ring :
-    hom-set-Large-Poset id
+    hom-set-Large-Poset
+      ( λ l → l)
       ( radical-ideal-Commutative-Ring-Large-Poset A)
       ( ideal-Commutative-Ring-Large-Poset A)
   map-hom-Large-Preorder
diff --git a/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md b/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md
index b954547a45..7fc1083b49 100644
--- a/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md
+++ b/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md
@@ -238,7 +238,8 @@ module _
         ( H))
 
   radical-of-ideal-hom-large-poset-Commutative-Ring :
-    hom-set-Large-Poset id
+    hom-set-Large-Poset
+      ( λ l → l)
       ( ideal-Commutative-Ring-Large-Poset A)
       ( radical-ideal-Commutative-Ring-Large-Poset A)
   map-hom-Large-Preorder
@@ -276,7 +277,7 @@ module _
     is-radical-of-ideal-radical-of-ideal-Commutative-Ring A I J
 
   radical-of-ideal-galois-connection-Commutative-Ring :
-    galois-connection-Large-Poset id id
+    galois-connection-Large-Poset (λ l → l) (λ l → l)
       ( ideal-Commutative-Ring-Large-Poset A)
       ( radical-ideal-Commutative-Ring-Large-Poset A)
   lower-adjoint-galois-connection-Large-Poset
diff --git a/src/foundation-core/functoriality-function-types.lagda.md b/src/foundation-core/functoriality-function-types.lagda.md
index 7f14cbd657..731efa774f 100644
--- a/src/foundation-core/functoriality-function-types.lagda.md
+++ b/src/foundation-core/functoriality-function-types.lagda.md
@@ -290,7 +290,8 @@ is-equiv-is-equiv-precomp-Prop :
   ({l : Level} (R : Prop l) → is-equiv (precomp f (type-Prop R))) →
   is-equiv f
 is-equiv-is-equiv-precomp-Prop P Q f H =
-  is-equiv-is-equiv-precomp-subuniverse id (λ l → is-prop) P Q f (λ l → H {l})
+  is-equiv-is-equiv-precomp-subuniverse
+    ( λ l → l) (λ l → is-prop) P Q f (λ l → H {l})
 
 is-equiv-is-equiv-precomp-Set :
   {l1 l2 : Level} (A : Set l1) (B : Set l2)
@@ -298,7 +299,8 @@ is-equiv-is-equiv-precomp-Set :
   ({l : Level} (C : Set l) → is-equiv (precomp f (type-Set C))) →
   is-equiv f
 is-equiv-is-equiv-precomp-Set A B f H =
-  is-equiv-is-equiv-precomp-subuniverse id (λ l → is-set) A B f (λ l → H {l})
+  is-equiv-is-equiv-precomp-subuniverse
+    ( λ l → l) (λ l → is-set) A B f (λ l → H {l})
 
 is-equiv-is-equiv-precomp-Truncated-Type :
   {l1 l2 : Level} (k : 𝕋)
@@ -307,7 +309,7 @@ is-equiv-is-equiv-precomp-Truncated-Type :
   ({l : Level} (C : Truncated-Type l k) → is-equiv (precomp f (pr1 C))) →
   is-equiv f
 is-equiv-is-equiv-precomp-Truncated-Type k A B f H =
-    is-equiv-is-equiv-precomp-subuniverse id (λ l → is-trunc k) A B f
+    is-equiv-is-equiv-precomp-subuniverse (λ l → l) (λ l → is-trunc k) A B f
       ( λ l → H {l})
 ```
 
diff --git a/src/foundation/connected-components-universes.lagda.md b/src/foundation/connected-components-universes.lagda.md
index b84f99d59f..52173ba92d 100644
--- a/src/foundation/connected-components-universes.lagda.md
+++ b/src/foundation/connected-components-universes.lagda.md
@@ -179,7 +179,7 @@ abstract
     is-contr-component-UU-Level-empty lzero
 ```
 
-### The connected components of universes are 0 connected
+### The connected components of universes are `0`-connected
 
 ```agda
 abstract
diff --git a/src/foundation/subuniverses.lagda.md b/src/foundation/subuniverses.lagda.md
index 2cfa64f9c4..385f0a1ed1 100644
--- a/src/foundation/subuniverses.lagda.md
+++ b/src/foundation/subuniverses.lagda.md
@@ -143,8 +143,7 @@ module _
   (α : Level → Level) (P : global-subuniverse α)
   where
 
-  is-in-global-subuniverse :
-    {l : Level} → UU l → UU (α l)
+  is-in-global-subuniverse : {l : Level} → UU l → UU (α l)
   is-in-global-subuniverse X =
     is-in-subuniverse (subuniverse-global-subuniverse P _) X
 ```
diff --git a/src/group-theory/cores-monoids.lagda.md b/src/group-theory/cores-monoids.lagda.md
index 7a6109893d..6217629d86 100644
--- a/src/group-theory/cores-monoids.lagda.md
+++ b/src/group-theory/cores-monoids.lagda.md
@@ -226,7 +226,9 @@ module _
 
 ```agda
 core-monoid-functor-Large-Precategory :
-  functor-Large-Precategory id Monoid-Large-Precategory Group-Large-Precategory
+  functor-Large-Precategory (λ l → l)
+    Monoid-Large-Precategory
+    Group-Large-Precategory
 obj-functor-Large-Precategory
   core-monoid-functor-Large-Precategory =
   core-Monoid
diff --git a/src/group-theory/normal-closures-subgroups.lagda.md b/src/group-theory/normal-closures-subgroups.lagda.md
index 86131f9e8d..99057b4147 100644
--- a/src/group-theory/normal-closures-subgroups.lagda.md
+++ b/src/group-theory/normal-closures-subgroups.lagda.md
@@ -252,7 +252,7 @@ module _
   normal-closure-Galois-Connection :
     galois-connection-Large-Poset
       ( λ l2 → l1 ⊔ l2)
-      ( id)
+      ( λ l → l)
       ( Subgroup-Large-Poset G)
       ( Normal-Subgroup-Large-Poset G)
   normal-closure-Galois-Connection =
diff --git a/src/group-theory/normal-cores-subgroups.lagda.md b/src/group-theory/normal-cores-subgroups.lagda.md
index 5005868a47..bd3f67d570 100644
--- a/src/group-theory/normal-cores-subgroups.lagda.md
+++ b/src/group-theory/normal-cores-subgroups.lagda.md
@@ -224,7 +224,7 @@ module _
 
   normal-core-subgroup-Galois-Connection :
     galois-connection-Large-Poset
-      ( id)
+      ( λ l → l)
       ( λ l2 → l1 ⊔ l2)
       ( Normal-Subgroup-Large-Poset G)
       ( Subgroup-Large-Poset G)
diff --git a/src/group-theory/normal-subgroups.lagda.md b/src/group-theory/normal-subgroups.lagda.md
index b701eb644f..9f808dbcc8 100644
--- a/src/group-theory/normal-subgroups.lagda.md
+++ b/src/group-theory/normal-subgroups.lagda.md
@@ -382,7 +382,8 @@ preserves-order-subgroup-Normal-Subgroup G N M = id
 
 subgroup-normal-subgroup-hom-Large-Poset :
   {l1 : Level} (G : Group l1) →
-  hom-set-Large-Poset id
+  hom-set-Large-Poset
+    ( λ l → l)
     ( Normal-Subgroup-Large-Poset G)
     ( Subgroup-Large-Poset G)
 subgroup-normal-subgroup-hom-Large-Poset G =
diff --git a/src/group-theory/subgroups-generated-by-subsets-groups.lagda.md b/src/group-theory/subgroups-generated-by-subsets-groups.lagda.md
index 5ed417a8d1..a99f441305 100644
--- a/src/group-theory/subgroups-generated-by-subsets-groups.lagda.md
+++ b/src/group-theory/subgroups-generated-by-subsets-groups.lagda.md
@@ -373,7 +373,7 @@ module _
   subgroup-subset-galois-connection-Group :
     galois-connection-Large-Poset
       ( λ l2 → l1 ⊔ l2)
-      ( id)
+      ( λ l → l)
       ( powerset-Large-Poset (type-Group G))
       ( Subgroup-Large-Poset G)
   lower-adjoint-galois-connection-Large-Poset
diff --git a/src/group-theory/subgroups.lagda.md b/src/group-theory/subgroups.lagda.md
index 3d14733150..11e5b5625e 100644
--- a/src/group-theory/subgroups.lagda.md
+++ b/src/group-theory/subgroups.lagda.md
@@ -490,7 +490,7 @@ preserves-order-subset-Subgroup G H K = id
 subset-subgroup-hom-large-poset-Group :
   {l1 : Level} (G : Group l1) →
   hom-set-Large-Poset
-    ( id)
+    ( λ l → l)
     ( Subgroup-Large-Poset G)
     ( powerset-Large-Poset (type-Group G))
 map-hom-Large-Preorder
diff --git a/src/group-theory/substitution-functor-group-actions.lagda.md b/src/group-theory/substitution-functor-group-actions.lagda.md
index 7b573d77db..be5225381f 100644
--- a/src/group-theory/substitution-functor-group-actions.lagda.md
+++ b/src/group-theory/substitution-functor-group-actions.lagda.md
@@ -86,7 +86,7 @@ module _
   preserves-comp-subst-Abstract-Group-Action X Y Z g f = refl
 
   subst-Abstract-Group-Action :
-    functor-Large-Precategory id
+    functor-Large-Precategory (λ l → l)
       ( Abstract-Group-Action-Large-Precategory H)
       ( Abstract-Group-Action-Large-Precategory G)
   obj-functor-Large-Precategory subst-Abstract-Group-Action =
diff --git a/src/order-theory/closure-operators-large-locales.lagda.md b/src/order-theory/closure-operators-large-locales.lagda.md
index 7c20d16e68..ed34d62d05 100644
--- a/src/order-theory/closure-operators-large-locales.lagda.md
+++ b/src/order-theory/closure-operators-large-locales.lagda.md
@@ -63,7 +63,8 @@ module _
     where
 
     hom-large-poset-closure-operator-Large-Locale :
-      hom-set-Large-Poset id
+      hom-set-Large-Poset
+        ( λ l → l)
         ( large-poset-Large-Locale L)
         ( large-poset-Large-Locale L)
     hom-large-poset-closure-operator-Large-Locale =
diff --git a/src/order-theory/closure-operators-large-posets.lagda.md b/src/order-theory/closure-operators-large-posets.lagda.md
index 2754468f56..5c2fed2f49 100644
--- a/src/order-theory/closure-operators-large-posets.lagda.md
+++ b/src/order-theory/closure-operators-large-posets.lagda.md
@@ -47,7 +47,7 @@ module _
     where
     field
       hom-closure-operator-Large-Poset :
-        hom-set-Large-Poset id P P
+        hom-set-Large-Poset (λ l → l) P P
       is-inflationary-closure-operator-Large-Poset :
         {l1 : Level} (x : type-Large-Poset P l1) →
         leq-Large-Poset P x
diff --git a/src/order-theory/galois-connections-large-posets.lagda.md b/src/order-theory/galois-connections-large-posets.lagda.md
index 40f3993a3f..98e4ac5e41 100644
--- a/src/order-theory/galois-connections-large-posets.lagda.md
+++ b/src/order-theory/galois-connections-large-posets.lagda.md
@@ -22,8 +22,8 @@ open import order-theory.order-preserving-maps-large-posets
 A **galois connection** between [large posets](order-theory.large-posets.md) `P`
 and `Q` consists of
 [order preserving maps](order-theory.order-preserving-maps-large-posets.md)
-`f : hom-set-Large-Poset id P Q` and `hom-set-Large-Poset id Q P` such that the
-adjoint relation
+`f : hom-set-Large-Poset (λ l → l) P Q` and `hom-set-Large-Poset id Q P` such
+that the adjoint relation
 
 ```text
   (f x ≤ y) ↔ (x ≤ g y)
diff --git a/src/order-theory/homomorphisms-large-meet-semilattices.lagda.md b/src/order-theory/homomorphisms-large-meet-semilattices.lagda.md
index 58ba75386a..19d1d2deaf 100644
--- a/src/order-theory/homomorphisms-large-meet-semilattices.lagda.md
+++ b/src/order-theory/homomorphisms-large-meet-semilattices.lagda.md
@@ -39,7 +39,8 @@ module _
     where
     field
       hom-large-poset-hom-Large-Meet-Semilattice :
-        hom-set-Large-Poset id
+        hom-set-Large-Poset
+          ( λ l → l)
           ( large-poset-Large-Meet-Semilattice K)
           ( large-poset-Large-Meet-Semilattice L)
       preserves-meets-hom-Large-Meet-Semilattice :
diff --git a/src/order-theory/homomorphisms-large-suplattices.lagda.md b/src/order-theory/homomorphisms-large-suplattices.lagda.md
index d13f3b7102..d68714dc51 100644
--- a/src/order-theory/homomorphisms-large-suplattices.lagda.md
+++ b/src/order-theory/homomorphisms-large-suplattices.lagda.md
@@ -35,7 +35,8 @@ module _
   where
 
   preserves-sup-hom-Large-Poset :
-    hom-set-Large-Poset id
+    hom-set-Large-Poset
+      ( λ l → l)
       ( large-poset-Large-Suplattice K)
       ( large-poset-Large-Suplattice L) →
     UUω
@@ -59,7 +60,8 @@ module _
     where
     field
       hom-large-poset-hom-Large-Suplattice :
-        hom-set-Large-Poset id
+        hom-set-Large-Poset
+          ( λ l → l)
           ( large-poset-Large-Suplattice K)
           ( large-poset-Large-Suplattice L)
       preserves-sup-hom-Large-Suplattice :
diff --git a/src/order-theory/nuclei-large-locales.lagda.md b/src/order-theory/nuclei-large-locales.lagda.md
index f4e94f161b..b62fdad6ec 100644
--- a/src/order-theory/nuclei-large-locales.lagda.md
+++ b/src/order-theory/nuclei-large-locales.lagda.md
@@ -35,8 +35,8 @@ open import order-theory.least-upper-bounds-large-posets
 ## Idea
 
 A **nucleus** on a [large locale](order-theory.large-locales.md) `L` is an order
-preserving map `j : hom-set-Large-Poset id L L` such that `j` preserves meets
-and is inflationary and idempotent.
+preserving map `j : hom-set-Large-Poset (λ l → l) L L` such that `j` preserves
+meets and is inflationary and idempotent.
 
 ## Definitions
 
diff --git a/src/ring-theory/ideals-generated-by-subsets-rings.lagda.md b/src/ring-theory/ideals-generated-by-subsets-rings.lagda.md
index 4f72a0479e..794b0633cf 100644
--- a/src/ring-theory/ideals-generated-by-subsets-rings.lagda.md
+++ b/src/ring-theory/ideals-generated-by-subsets-rings.lagda.md
@@ -385,7 +385,7 @@ module _
 
   ideal-subset-galois-connection-Ring :
     galois-connection-Large-Poset
-      ( _⊔_ l1) id
+      ( _⊔_ l1) (λ l → l)
       ( powerset-Large-Poset (type-Ring A))
       ( ideal-Ring-Large-Poset A)
   lower-adjoint-galois-connection-Large-Poset
diff --git a/src/ring-theory/left-ideals-generated-by-subsets-rings.lagda.md b/src/ring-theory/left-ideals-generated-by-subsets-rings.lagda.md
index a506870555..d1060ba3ae 100644
--- a/src/ring-theory/left-ideals-generated-by-subsets-rings.lagda.md
+++ b/src/ring-theory/left-ideals-generated-by-subsets-rings.lagda.md
@@ -341,7 +341,7 @@ module _
 
   left-ideal-subset-galois-connection-Ring :
     galois-connection-Large-Poset
-      ( _⊔_ l1) id
+      ( l1 ⊔_) (λ l → l)
       ( powerset-Large-Poset (type-Ring A))
       ( left-ideal-Ring-Large-Poset A)
   lower-adjoint-galois-connection-Large-Poset
diff --git a/src/ring-theory/poset-of-ideals-rings.lagda.md b/src/ring-theory/poset-of-ideals-rings.lagda.md
index 8f29c36673..6fb53bd08a 100644
--- a/src/ring-theory/poset-of-ideals-rings.lagda.md
+++ b/src/ring-theory/poset-of-ideals-rings.lagda.md
@@ -152,7 +152,7 @@ module _
 
   subset-ideal-hom-large-poset-Ring :
     hom-set-Large-Poset
-      ( id)
+      ( λ l → l)
       ( ideal-Ring-Large-Poset R)
       ( powerset-Large-Poset (type-Ring R))
   map-hom-Large-Preorder subset-ideal-hom-large-poset-Ring =
diff --git a/src/ring-theory/poset-of-left-ideals-rings.lagda.md b/src/ring-theory/poset-of-left-ideals-rings.lagda.md
index 87fda7dfea..133aac4fcb 100644
--- a/src/ring-theory/poset-of-left-ideals-rings.lagda.md
+++ b/src/ring-theory/poset-of-left-ideals-rings.lagda.md
@@ -162,7 +162,7 @@ module _
 
   subset-left-ideal-hom-large-poset-Ring :
     hom-set-Large-Poset
-      ( id)
+      ( λ l → l)
       ( left-ideal-Ring-Large-Poset R)
       ( powerset-Large-Poset (type-Ring R))
   map-hom-Large-Preorder subset-left-ideal-hom-large-poset-Ring =
diff --git a/src/ring-theory/poset-of-right-ideals-rings.lagda.md b/src/ring-theory/poset-of-right-ideals-rings.lagda.md
index 7911bdafab..64d4e54ecc 100644
--- a/src/ring-theory/poset-of-right-ideals-rings.lagda.md
+++ b/src/ring-theory/poset-of-right-ideals-rings.lagda.md
@@ -163,7 +163,7 @@ module _
 
   subset-right-ideal-hom-large-poset-Ring :
     hom-set-Large-Poset
-      ( id)
+      ( λ l → l)
       ( right-ideal-Ring-Large-Poset R)
       ( powerset-Large-Poset (type-Ring R))
   map-hom-Large-Preorder subset-right-ideal-hom-large-poset-Ring =
diff --git a/src/ring-theory/right-ideals-generated-by-subsets-rings.lagda.md b/src/ring-theory/right-ideals-generated-by-subsets-rings.lagda.md
index 237aaa0d0a..041d821bfe 100644
--- a/src/ring-theory/right-ideals-generated-by-subsets-rings.lagda.md
+++ b/src/ring-theory/right-ideals-generated-by-subsets-rings.lagda.md
@@ -339,7 +339,7 @@ module _
 
   right-ideal-subset-galois-connection-Ring :
     galois-connection-Large-Poset
-      ( _⊔_ l1) id
+      ( l1 ⊔_) (λ l → l)
       ( powerset-Large-Poset (type-Ring A))
       ( right-ideal-Ring-Large-Poset A)
   lower-adjoint-galois-connection-Large-Poset
diff --git a/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md
index 3a83b52b38..4ba67acf23 100644
--- a/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md
@@ -58,7 +58,7 @@ coefficients of the composite of the Cauchy series of `S` and `T`.
 module _
   {l1 l2 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   where
 
   type-cauchy-composition-species-subuniverse :
@@ -83,13 +83,13 @@ module _
     ( S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
     ( T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
     ( X : type-subuniverse P) →
-    is-in-global-subuniverse id Q
+    is-in-global-subuniverse (λ l → l) Q
       ( type-cauchy-composition-species-subuniverse S T X)
 
 module _
   {l1 l2 l3 l4 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (C1 : is-closed-under-cauchy-composition-species-subuniverse P Q)
   (C2 : is-closed-under-Σ-subuniverse P)
   (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
@@ -112,7 +112,7 @@ module _
 module _
   {l1 l2 l3 l4 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (C1 : is-closed-under-cauchy-composition-species-subuniverse P Q)
   (C2 : is-closed-under-Σ-subuniverse P)
   (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
@@ -185,7 +185,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l))
   ( C3 : is-in-subuniverse P (raise-unit l1))
   ( C4 :
     is-closed-under-is-contr-subuniverses P
@@ -249,7 +249,7 @@ module _
 module _
   { l1 l2 l3 : Level}
   ( P : subuniverse l1 l2)
-  ( Q : global-subuniverse id)
+  ( Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-cauchy-composition-species-subuniverse P Q)
   ( C2 : is-closed-under-Σ-subuniverse P)
   ( C3 : is-in-subuniverse P (raise-unit l1))
@@ -366,7 +366,7 @@ module _
 module _
   { l1 l2 l3 l4 l5 : Level}
   ( P : subuniverse l1 l2)
-  ( Q : global-subuniverse id)
+  ( Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-cauchy-composition-species-subuniverse P Q)
   ( C2 : is-closed-under-Σ-subuniverse P)
   ( S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
diff --git a/src/species/cauchy-exponentials-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-exponentials-species-of-types-in-subuniverses.lagda.md
index f308e753bc..79dd6514a7 100644
--- a/src/species/cauchy-exponentials-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/cauchy-exponentials-species-of-types-in-subuniverses.lagda.md
@@ -57,7 +57,7 @@ the Cauchy exponential is also a species of types in subuniverse from `P` to
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l))
   where
 
   type-cauchy-exponential-species-subuniverse :
@@ -76,7 +76,7 @@ module _
 
 ```agda
 is-closed-under-cauchy-exponential-species-subuniverse :
-  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id) →
+  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l)) →
   UUω
 is-closed-under-cauchy-exponential-species-subuniverse {l1} {l2} P Q =
   {l3 : Level}
@@ -91,7 +91,7 @@ is-closed-under-cauchy-exponential-species-subuniverse {l1} {l2} P Q =
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-cauchy-exponential-species-subuniverse P Q)
   where
 
@@ -111,7 +111,7 @@ module _
 module _
   {l1 l2 l3 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (C1 : is-closed-under-cauchy-exponential-species-subuniverse P Q)
   (C2 : is-in-subuniverse (subuniverse-global-subuniverse Q lzero) unit)
   (C3 : is-closed-under-cauchy-composition-species-subuniverse P Q)
@@ -136,7 +136,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-cauchy-exponential-species-subuniverse P Q)
   ( C2 :
     ( U : UU l1) →
@@ -243,7 +243,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
+  ( Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-cauchy-exponential-species-subuniverse P Q)
   ( C2 : is-closed-under-coproduct-species-subuniverse P Q)
   ( C3 : is-closed-under-cauchy-product-species-subuniverse P Q)
diff --git a/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md
index 03ad6b59e3..aa6eb35865 100644
--- a/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md
@@ -51,7 +51,8 @@ the Cauchy product is also a species of subuniverse from `P` to `Q`.
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
+  (Q : global-subuniverse (λ l → l))
   where
 
   type-cauchy-product-species-subuniverse :
@@ -73,7 +74,7 @@ module _
 
 ```agda
 is-closed-under-cauchy-product-species-subuniverse :
-  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id) →
+  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l)) →
   UUω
 is-closed-under-cauchy-product-species-subuniverse {l1} {l2} P Q =
   {l3 l4 : Level}
@@ -89,7 +90,8 @@ is-closed-under-cauchy-product-species-subuniverse {l1} {l2} P Q =
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
+  (Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-cauchy-product-species-subuniverse P Q)
   where
 
@@ -109,7 +111,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 l5 : Level} (P : subuniverse l1 l2)
+  (Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-cauchy-product-species-subuniverse P Q)
   ( C2 : is-closed-under-coproducts-subuniverse P)
   where
@@ -246,7 +249,7 @@ module _
 module _
   {l1 l2 l3 l4 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (C1 : is-closed-under-cauchy-product-species-subuniverse P Q)
   (S : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
   (T : species-subuniverse P ( subuniverse-global-subuniverse Q l4))
@@ -289,7 +292,7 @@ unit-cauchy-product-species-subuniverse P Q C X =
   is-empty (inclusion-subuniverse P X) , C X
 
 module _
-  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l))
   (C1 : is-closed-under-cauchy-product-species-subuniverse P Q)
   (C2 : is-in-subuniverse P (raise-empty l1))
   (C3 :
@@ -372,7 +375,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
+  (Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-cauchy-product-species-subuniverse P Q)
   ( C2 : is-closed-under-coproducts-subuniverse P)
   (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
diff --git a/src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md
index d296ac285f..1e26789778 100644
--- a/src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md
@@ -79,7 +79,7 @@ module _
 module _
   {l1 l2 l3 l4 l5 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
   (T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
   (f :
diff --git a/src/species/composition-cauchy-series-species-of-types-in-subuniverses.lagda.md b/src/species/composition-cauchy-series-species-of-types-in-subuniverses.lagda.md
index a8f38abd1c..d450b631b7 100644
--- a/src/species/composition-cauchy-series-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/composition-cauchy-series-species-of-types-in-subuniverses.lagda.md
@@ -35,7 +35,7 @@ at `X`
 module _
   {l1 l2 l3 l4 l5 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
   (T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
   (X : UU l5)
@@ -63,7 +63,7 @@ module _
 module _
   {l1 l2 l3 l4 l5 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
   (T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
   (X : UU l5)
@@ -122,7 +122,7 @@ module _
 module _
   {l1 l2 l3 l4 l5 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (C1 : is-closed-under-cauchy-composition-species-subuniverse P Q)
   (C2 : is-closed-under-Σ-subuniverse P)
   (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
diff --git a/src/species/coproducts-species-of-types-in-subuniverses.lagda.md b/src/species/coproducts-species-of-types-in-subuniverses.lagda.md
index 2a1a752588..772765aa8d 100644
--- a/src/species/coproducts-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/coproducts-species-of-types-in-subuniverses.lagda.md
@@ -34,7 +34,8 @@ stable by coproduct.
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
+  (Q : global-subuniverse (λ l → l))
   where
 
   type-coproduct-species-subuniverse :
@@ -54,7 +55,7 @@ module _
 
 ```agda
 is-closed-under-coproduct-species-subuniverse :
-  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id) →
+  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l)) →
   UUω
 is-closed-under-coproduct-species-subuniverse P Q =
   {l3 l4 : Level}
@@ -70,7 +71,8 @@ is-closed-under-coproduct-species-subuniverse P Q =
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
+  (Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-coproduct-species-subuniverse P Q)
   where
 
@@ -89,7 +91,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
+  ( Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-coproduct-species-subuniverse P Q)
   ( S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
   ( T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
diff --git a/src/species/dirichlet-exponentials-species-of-types-in-subuniverses.lagda.md b/src/species/dirichlet-exponentials-species-of-types-in-subuniverses.lagda.md
index d581585b1f..8388c10511 100644
--- a/src/species/dirichlet-exponentials-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/dirichlet-exponentials-species-of-types-in-subuniverses.lagda.md
@@ -53,7 +53,7 @@ the Dirichlet exponential is also a species of types in subuniverse from `P` to
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l))
   where
 
   type-dirichlet-exponential-species-subuniverse :
@@ -72,7 +72,7 @@ module _
 
 ```agda
 is-closed-under-dirichlet-exponential-species-subuniverse :
-  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id) →
+  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l)) →
   UUω
 is-closed-under-dirichlet-exponential-species-subuniverse {l1} {l2} P Q =
   {l3 : Level}
@@ -87,7 +87,7 @@ is-closed-under-dirichlet-exponential-species-subuniverse {l1} {l2} P Q =
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-dirichlet-exponential-species-subuniverse P Q)
   where
 
@@ -105,7 +105,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-dirichlet-exponential-species-subuniverse P Q)
   ( C2 :
     ( U : UU l1) →
@@ -212,7 +212,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
+  (Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-dirichlet-exponential-species-subuniverse P Q)
   ( C2 : is-closed-under-coproduct-species-subuniverse P Q)
   ( C3 : is-closed-under-dirichlet-product-species-subuniverse P Q)
diff --git a/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md b/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md
index 71bdd90718..ab0927bdf0 100644
--- a/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md
@@ -50,7 +50,8 @@ dirichlet product is also a species of subuniverse from `P` to `Q`
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
+  (Q : global-subuniverse (λ l → l))
   where
 
   type-dirichlet-product-species-subuniverse :
@@ -70,7 +71,7 @@ module _
 
 ```agda
 is-closed-under-dirichlet-product-species-subuniverse :
-  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id) →
+  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l)) →
   UUω
 is-closed-under-dirichlet-product-species-subuniverse {l1} {l2} P Q =
   {l3 l4 : Level}
@@ -86,7 +87,8 @@ is-closed-under-dirichlet-product-species-subuniverse {l1} {l2} P Q =
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
+  (Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
   where
 
@@ -106,7 +108,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 l5 : Level} (P : subuniverse l1 l2)
+  ( Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
   ( C2 : is-closed-under-products-subuniverse P)
   where
@@ -274,7 +277,7 @@ module _
 module _
   {l1 l2 l3 l4 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
   (S : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
   (T : species-subuniverse P ( subuniverse-global-subuniverse Q l4))
@@ -318,7 +321,7 @@ unit-dirichlet-product-species-subuniverse P Q C X =
   is-contr (inclusion-subuniverse P X) , C X
 
 module _
-  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l))
   (C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
   (C2 : is-in-subuniverse P (raise-unit l1))
   (C3 :
@@ -403,7 +406,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
+  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
+  ( Q : global-subuniverse (λ l → l))
   ( C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
   ( C2 : is-closed-under-products-subuniverse P)
   (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
diff --git a/src/species/exponentials-cauchy-series-of-types-in-subuniverses.lagda.md b/src/species/exponentials-cauchy-series-of-types-in-subuniverses.lagda.md
index aede799076..0977660ef0 100644
--- a/src/species/exponentials-cauchy-series-of-types-in-subuniverses.lagda.md
+++ b/src/species/exponentials-cauchy-series-of-types-in-subuniverses.lagda.md
@@ -58,7 +58,7 @@ module _
 module _
   {l1 l2 l3 l5 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (C : is-in-subuniverse (subuniverse-global-subuniverse Q lzero) unit)
   (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
   (X : UU l5)
@@ -81,7 +81,7 @@ module _
 module _
   {l1 l2 l3 l4 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (C1 : is-closed-under-cauchy-exponential-species-subuniverse P Q)
   (C2 : is-in-subuniverse (subuniverse-global-subuniverse Q lzero) unit)
   (C3 : is-closed-under-cauchy-composition-species-subuniverse P Q)
diff --git a/src/species/products-cauchy-series-species-of-types-in-subuniverses.lagda.md b/src/species/products-cauchy-series-species-of-types-in-subuniverses.lagda.md
index 8cc4b98260..a9a15785e4 100644
--- a/src/species/products-cauchy-series-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/products-cauchy-series-species-of-types-in-subuniverses.lagda.md
@@ -35,7 +35,7 @@ The product of two Cauchy series is just the pointwise product.
 module _
   {l1 l2 l3 l4 l5 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
   (T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
   (X : UU l5)
@@ -58,7 +58,7 @@ module _
 module _
   {l1 l2 l3 l4 l5 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
   (T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
   (X : UU l5)
@@ -99,7 +99,7 @@ module _
 module _
   {l1 l2 l3 l4 l5 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (C1 : is-closed-under-cauchy-product-species-subuniverse P Q)
   (C2 : is-closed-under-coproducts-subuniverse P)
   (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
diff --git a/src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md b/src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md
index 4225837e5e..1547e49145 100644
--- a/src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md
@@ -38,7 +38,7 @@ The product of two Dirichlet series is the pointwise product.
 module _
   {l1 l2 l3 l4 l5 l6 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (C1 : is-closed-under-products-subuniverse P)
   (H : species-subuniverse-domain l5 P)
   (C2 : preserves-product-species-subuniverse-domain P C1 H)
@@ -76,7 +76,7 @@ module _
 module _
   {l1 l2 l3 l4 l5 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (C1 : is-closed-under-products-subuniverse P)
   (H : species-subuniverse-domain l5 P)
   (C2 : preserves-product-species-subuniverse-domain P C1 H)
diff --git a/src/species/unit-cauchy-composition-species-of-types-in-subuniverses.lagda.md b/src/species/unit-cauchy-composition-species-of-types-in-subuniverses.lagda.md
index 8721a6b7e3..2a11af1ba0 100644
--- a/src/species/unit-cauchy-composition-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/unit-cauchy-composition-species-of-types-in-subuniverses.lagda.md
@@ -33,7 +33,7 @@ Cauchy composition of species of types in a subuniverse by
 module _
   {l1 l2 : Level}
   (P : subuniverse l1 l2)
-  (Q : global-subuniverse id)
+  (Q : global-subuniverse (λ l → l))
   (C4 :
     is-closed-under-is-contr-subuniverses P
       ( subuniverse-global-subuniverse Q l1))