chore: Remove redundant parentheses in universe level expressions (#1125

)
UniMath · Apr 20, 2024 · b9cf844 · b9cf844
1 parent cebf28e
commit b9cf844
Show file tree

Hide file tree

Showing 19 changed files with 26 additions and 26 deletions.
diff --git a/src/commutative-algebra/subsets-commutative-rings.lagda.md b/src/commutative-algebra/subsets-commutative-rings.lagda.md
@@ -33,7 +33,7 @@ A **subset** of a commutative ring is a subtype of its underlying type.
 
 ```agda
 subset-Commutative-Ring :
-  (l : Level) {l1 : Level} (A : Commutative-Ring l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (A : Commutative-Ring l1) → UU (lsuc l ⊔ l1)
 subset-Commutative-Ring l A = subtype l (type-Commutative-Ring A)
 
 is-set-subset-Commutative-Ring :

diff --git a/src/commutative-algebra/subsets-commutative-semirings.lagda.md b/src/commutative-algebra/subsets-commutative-semirings.lagda.md
@@ -30,7 +30,7 @@ A **subset** of a commutative semiring is a subtype of its underlying type.
 
 ```agda
 subset-Commutative-Semiring :
-  (l : Level) {l1 : Level} (A : Commutative-Semiring l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (A : Commutative-Semiring l1) → UU (lsuc l ⊔ l1)
 subset-Commutative-Semiring l A =
   subset-Semiring l (semiring-Commutative-Semiring A)
 

diff --git a/src/foundation-core/equivalence-relations.lagda.md b/src/foundation-core/equivalence-relations.lagda.md
@@ -38,7 +38,7 @@ is-equivalence-relation R =
   is-transitive-Relation-Prop R
 
 equivalence-relation :
-  (l : Level) {l1 : Level} (A : UU l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1)
 equivalence-relation l A = Σ (Relation-Prop l A) is-equivalence-relation
 
 prop-equivalence-relation :

diff --git a/src/foundation/binary-relations.lagda.md b/src/foundation/binary-relations.lagda.md
@@ -51,7 +51,7 @@ total-space-Relation {A = A} R = Σ (A × A) λ (a , a') → R a a'
 
 ```agda
 Relation-Prop :
-  (l : Level) {l1 : Level} (A : UU l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1)
 Relation-Prop l A = A → A → Prop l
 
 type-Relation-Prop :

diff --git a/src/foundation/large-locale-of-subtypes.lagda.md b/src/foundation/large-locale-of-subtypes.lagda.md
@@ -38,11 +38,11 @@ module _
   where
 
   powerset-Large-Locale :
-    Large-Locale (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ (l2 ⊔ l3)) lzero
+    Large-Locale (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3) lzero
   powerset-Large-Locale = power-Large-Locale A Prop-Large-Locale
 
   large-poset-powerset-Large-Locale :
-    Large-Poset (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ (l2 ⊔ l3))
+    Large-Poset (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
   large-poset-powerset-Large-Locale =
     large-poset-Large-Locale powerset-Large-Locale
 
@@ -60,12 +60,12 @@ module _
     is-set-type-Large-Locale powerset-Large-Locale
 
   large-meet-semilattice-powerset-Large-Locale :
-    Large-Meet-Semilattice (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ (l2 ⊔ l3))
+    Large-Meet-Semilattice (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
   large-meet-semilattice-powerset-Large-Locale =
     large-meet-semilattice-Large-Locale powerset-Large-Locale
 
   large-suplattice-powerset-Large-Locale :
-    Large-Suplattice (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ (l2 ⊔ l3)) lzero
+    Large-Suplattice (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3) lzero
   large-suplattice-powerset-Large-Locale =
     large-suplattice-Large-Locale powerset-Large-Locale
 

diff --git a/src/foundation/subuniverses.lagda.md b/src/foundation/subuniverses.lagda.md
@@ -38,7 +38,7 @@ open import foundation-core.transport-along-identifications
 
 ```agda
 is-subuniverse :
-  {l1 l2 : Level} (P : UU l1 → UU l2) → UU ((lsuc l1) ⊔ l2)
+  {l1 l2 : Level} (P : UU l1 → UU l2) → UU (lsuc l1 ⊔ l2)
 is-subuniverse P = is-subtype P
 
 subuniverse :

diff --git a/src/group-theory/decidable-subgroups.lagda.md b/src/group-theory/decidable-subgroups.lagda.md
@@ -41,7 +41,7 @@ predicate on the type of elements of `G`.
 
 ```agda
 decidable-subset-Group :
-  (l : Level) {l1 : Level} (G : Group l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (G : Group l1) → UU (lsuc l ⊔ l1)
 decidable-subset-Group l G = decidable-subtype l (type-Group G)
 
 is-set-decidable-subset-Group :
@@ -121,7 +121,7 @@ module _
     is-prop-is-subgroup-subset-Group G (subset-decidable-subset-Group G P)
 
 Decidable-Subgroup :
-  (l : Level) {l1 : Level} (G : Group l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (G : Group l1) → UU (lsuc l ⊔ l1)
 Decidable-Subgroup l G =
   type-subtype (is-subgroup-prop-decidable-subset-Group {l2 = l} G)
 

diff --git a/src/group-theory/embeddings-abelian-groups.lagda.md b/src/group-theory/embeddings-abelian-groups.lagda.md
@@ -53,7 +53,7 @@ module _
 
 ```agda
 emb-Ab-Slice :
-  (l : Level) {l1 : Level} (A : Ab l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (A : Ab l1) → UU (lsuc l ⊔ l1)
 emb-Ab-Slice l A = emb-Group-Slice l (group-Ab A)
 
 emb-ab-slice-Subgroup-Ab :

diff --git a/src/group-theory/embeddings-groups.lagda.md b/src/group-theory/embeddings-groups.lagda.md
@@ -52,7 +52,7 @@ module _
 
 ```agda
 emb-Group-Slice :
-  (l : Level) {l1 : Level} (G : Group l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (G : Group l1) → UU (lsuc l ⊔ l1)
 emb-Group-Slice l G = Σ ( Group l) (λ H → emb-Group H G)
 
 emb-group-slice-Subgroup :

diff --git a/src/group-theory/subgroups-abelian-groups.lagda.md b/src/group-theory/subgroups-abelian-groups.lagda.md
@@ -81,7 +81,7 @@ module _
 
 ```agda
 Subgroup-Ab :
-  (l : Level) {l1 : Level} (A : Ab l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (A : Ab l1) → UU (lsuc l ⊔ l1)
 Subgroup-Ab l A = Subgroup l (group-Ab A)
 
 module _

diff --git a/src/group-theory/subsets-abelian-groups.lagda.md b/src/group-theory/subsets-abelian-groups.lagda.md
@@ -59,7 +59,7 @@ module _
 
 ```agda
 subset-Ab :
-  (l : Level) {l1 : Level} (A : Ab l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (A : Ab l1) → UU (lsuc l ⊔ l1)
 subset-Ab l A = subset-Group l (group-Ab A)
 
 is-set-subset-Ab :

diff --git a/src/group-theory/subsets-groups.lagda.md b/src/group-theory/subsets-groups.lagda.md
@@ -57,7 +57,7 @@ module _
 
 ```agda
 subset-Group :
-  (l : Level) {l1 : Level} (G : Group l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (G : Group l1) → UU (lsuc l ⊔ l1)
 subset-Group l G = type-Large-Locale (powerset-large-locale-Group G) l
 
 is-set-subset-Group :

diff --git a/src/ring-theory/ideals-rings.lagda.md b/src/ring-theory/ideals-rings.lagda.md
@@ -63,7 +63,7 @@ is-prop-is-ideal-subset-Ring R P =
       ( is-prop-is-closed-under-right-multiplication-subset-Ring R P))
 
 ideal-Ring :
-  (l : Level) {l1 : Level} (R : Ring l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (R : Ring l1) → UU (lsuc l ⊔ l1)
 ideal-Ring l R =
   Σ (subset-Ring l R) (is-ideal-subset-Ring R)
 

diff --git a/src/ring-theory/ideals-semirings.lagda.md b/src/ring-theory/ideals-semirings.lagda.md
@@ -63,7 +63,7 @@ module _
     is-closed-under-left-multiplication-subset-Semiring R P
 
 left-ideal-Semiring :
-  (l : Level) {l1 : Level} (R : Semiring l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (R : Semiring l1) → UU (lsuc l ⊔ l1)
 left-ideal-Semiring l R =
   Σ (subset-Semiring l R) (is-left-ideal-subset-Semiring R)
 
@@ -148,7 +148,7 @@ module _
     is-closed-under-right-multiplication-subset-Semiring R P
 
 right-ideal-Semiring :
-  (l : Level) {l1 : Level} (R : Semiring l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (R : Semiring l1) → UU (lsuc l ⊔ l1)
 right-ideal-Semiring l R =
   Σ (subset-Semiring l R) (is-right-ideal-subset-Semiring R)
 
@@ -231,7 +231,7 @@ is-ideal-subset-Semiring R P =
     is-closed-under-right-multiplication-subset-Semiring R P)
 
 ideal-Semiring :
-  (l : Level) {l1 : Level} (R : Semiring l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (R : Semiring l1) → UU (lsuc l ⊔ l1)
 ideal-Semiring l R =
   Σ (subset-Semiring l R) (is-ideal-subset-Semiring R)
 

diff --git a/src/ring-theory/left-ideals-rings.lagda.md b/src/ring-theory/left-ideals-rings.lagda.md
@@ -52,7 +52,7 @@ module _
       ( is-prop-is-closed-under-left-multiplication-subset-Ring R S)
 
 left-ideal-Ring :
-  (l : Level) {l1 : Level} (R : Ring l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (R : Ring l1) → UU (lsuc l ⊔ l1)
 left-ideal-Ring l R = Σ (subset-Ring l R) (is-left-ideal-subset-Ring R)
 
 module _

diff --git a/src/ring-theory/right-ideals-rings.lagda.md b/src/ring-theory/right-ideals-rings.lagda.md
@@ -52,7 +52,7 @@ module _
       ( is-prop-is-closed-under-right-multiplication-subset-Ring R S)
 
 right-ideal-Ring :
-  (l : Level) {l1 : Level} (R : Ring l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (R : Ring l1) → UU (lsuc l ⊔ l1)
 right-ideal-Ring l R = Σ (subset-Ring l R) (is-right-ideal-subset-Ring R)
 
 module _

diff --git a/src/ring-theory/subsets-rings.lagda.md b/src/ring-theory/subsets-rings.lagda.md
@@ -31,7 +31,7 @@ A subset of a ring is a subtype of the underlying type of a ring
 
 ```agda
 subset-Ring :
-  (l : Level) {l1 : Level} (R : Ring l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (R : Ring l1) → UU (lsuc l ⊔ l1)
 subset-Ring l R = subtype l (type-Ring R)
 
 is-set-subset-Ring :

diff --git a/src/ring-theory/subsets-semirings.lagda.md b/src/ring-theory/subsets-semirings.lagda.md
@@ -29,7 +29,7 @@ A subset of a semiring is a subtype of the underlying type of a semiring
 
 ```agda
 subset-Semiring :
-  (l : Level) {l1 : Level} (R : Semiring l1) → UU ((lsuc l) ⊔ l1)
+  (l : Level) {l1 : Level} (R : Semiring l1) → UU (lsuc l ⊔ l1)
 subset-Semiring l R = subtype l (type-Semiring R)
 
 is-set-subset-Semiring :

diff --git a/src/synthetic-homotopy-theory/universal-property-circle.lagda.md b/src/synthetic-homotopy-theory/universal-property-circle.lagda.md
@@ -74,7 +74,7 @@ module _
   {l1 : Level} (l2 : Level) {X : UU l1} (α : free-loop X)
   where
 
-  induction-principle-circle : UU ((lsuc l2) ⊔ l1)
+  induction-principle-circle : UU (lsuc l2 ⊔ l1)
   induction-principle-circle = (P : X → UU l2) → section (ev-free-loop-Π α P)
 
 module _
@@ -98,7 +98,7 @@ module _
   {l1 : Level} (l2 : Level) {X : UU l1} (α : free-loop X)
   where
 
-  dependent-universal-property-circle : UU ((lsuc l2) ⊔ l1)
+  dependent-universal-property-circle : UU (lsuc l2 ⊔ l1)
   dependent-universal-property-circle =
     (P : X → UU l2) → is-equiv (ev-free-loop-Π α P)
 ```