Level-universe compatibility patch

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)
 ```

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

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

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

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

src/foundation-core/functoriality-function-types.lagda.md

@@ -290,15 +290,17 @@ 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)
   (f : type-Set A → type-Set B) →
   ({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})
 ```
 

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

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
 ```

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

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 =

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)

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 =

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

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

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 =

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 =

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

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)

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 :

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 :

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
 

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

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

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 =

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 =

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 =

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

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))