Switch from 𝔽 to Finite-*

src/elementary-number-theory/eulers-totient-function.lagda.md

@@ -48,8 +48,8 @@ extend naturally to the first definition.
 ```agda
 eulers-totient-function-relatively-prime : ℕ → ℕ
 eulers-totient-function-relatively-prime n =
-  number-of-elements-subset-𝔽
-    ( Fin-𝔽 n)
+  number-of-elements-subset-Finite-Type
+    ( Fin-Finite-Type n)
     ( λ x → is-relatively-prime-ℕ-Decidable-Prop (nat-Fin n x) n)
 ```
 

src/elementary-number-theory/modular-arithmetic.lagda.md

@@ -130,9 +130,9 @@ abstract
   is-finite-ℤ-Mod {zero-ℕ} H = ex-falso (H refl)
   is-finite-ℤ-Mod {succ-ℕ k} H = is-finite-Fin (succ-ℕ k)
 
-ℤ-Mod-𝔽 : (k : ℕ) → is-nonzero-ℕ k → 𝔽 lzero
-pr1 (ℤ-Mod-𝔽 k H) = ℤ-Mod k
-pr2 (ℤ-Mod-𝔽 k H) = is-finite-ℤ-Mod H
+ℤ-Mod-Finite-Type : (k : ℕ) → is-nonzero-ℕ k → Finite-Type lzero
+pr1 (ℤ-Mod-Finite-Type k H) = ℤ-Mod k
+pr2 (ℤ-Mod-Finite-Type k H) = is-finite-ℤ-Mod H
 ```
 
 ## The inclusion of the integers modulo `k` into ℤ

src/elementary-number-theory/multiset-coefficients.lagda.md

@@ -21,7 +21,7 @@ words, it counts the number of
 [connected componets](foundation.connected-components.md) of the type
 
 ```text
-  Σ (A : Fin n → 𝔽), ║ Fin k ≃ Σ (i : Fin n), A i ║.
+  Σ (A : Fin n → Finite-Type), ║ Fin k ≃ Σ (i : Fin n), A i ║.
 ```
 
 The first few numbers are

src/finite-algebra/dependent-products-commutative-finite-rings.lagda.md

@@ -41,183 +41,199 @@ ring.
 
 ```agda
 module _
-  {l1 l2 : Level} (I : 𝔽 l1) (A : type-𝔽 I → Commutative-Ring-𝔽 l2)
+  {l1 l2 : Level} (I : Finite-Type l1)
+  (A : type-Finite-Type I → Finite-Commutative-Ring l2)
   where
 
-  finite-ring-Π-Commutative-Ring-𝔽 : Ring-𝔽 (l1 ⊔ l2)
-  finite-ring-Π-Commutative-Ring-𝔽 =
-    Π-Ring-𝔽 I (λ i → finite-ring-Commutative-Ring-𝔽 (A i))
+  finite-ring-Π-Finite-Commutative-Ring : Finite-Ring (l1 ⊔ l2)
+  finite-ring-Π-Finite-Commutative-Ring =
+    Π-Finite-Ring I (λ i → finite-ring-Finite-Commutative-Ring (A i))
 
-  ring-Π-Commutative-Ring-𝔽 : Ring (l1 ⊔ l2)
-  ring-Π-Commutative-Ring-𝔽 =
-    Π-Ring (type-𝔽 I) (ring-Commutative-Ring-𝔽 ∘ A)
+  ring-Π-Finite-Commutative-Ring : Ring (l1 ⊔ l2)
+  ring-Π-Finite-Commutative-Ring =
+    Π-Ring (type-Finite-Type I) (ring-Finite-Commutative-Ring ∘ A)
 
-  ab-Π-Commutative-Ring-𝔽 : Ab (l1 ⊔ l2)
-  ab-Π-Commutative-Ring-𝔽 =
-    ab-Π-Commutative-Ring (type-𝔽 I) (commutative-ring-Commutative-Ring-𝔽 ∘ A)
+  ab-Π-Finite-Commutative-Ring : Ab (l1 ⊔ l2)
+  ab-Π-Finite-Commutative-Ring =
+    ab-Π-Commutative-Ring
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
 
-  multiplicative-commutative-monoid-Π-Commutative-Ring-𝔽 :
+  multiplicative-commutative-monoid-Π-Finite-Commutative-Ring :
     Commutative-Monoid (l1 ⊔ l2)
-  multiplicative-commutative-monoid-Π-Commutative-Ring-𝔽 =
+  multiplicative-commutative-monoid-Π-Finite-Commutative-Ring =
     multiplicative-commutative-monoid-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
 
-  set-Π-Commutative-Ring-𝔽 : Set (l1 ⊔ l2)
-  set-Π-Commutative-Ring-𝔽 =
+  set-Π-Finite-Commutative-Ring : Set (l1 ⊔ l2)
+  set-Π-Finite-Commutative-Ring =
     set-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  type-Π-Commutative-Ring-𝔽 : UU (l1 ⊔ l2)
-  type-Π-Commutative-Ring-𝔽 =
-    type-Π-Commutative-Ring (type-𝔽 I) (commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  finite-type-Π-Commutative-Ring-𝔽 : 𝔽 (l1 ⊔ l2)
-  finite-type-Π-Commutative-Ring-𝔽 =
-    finite-type-Π-Ring-𝔽 I (finite-ring-Commutative-Ring-𝔽 ∘ A)
-
-  is-finite-type-Π-Commutative-Ring-𝔽 : is-finite type-Π-Commutative-Ring-𝔽
-  is-finite-type-Π-Commutative-Ring-𝔽 =
-    is-finite-type-Π-Ring-𝔽 I (finite-ring-Commutative-Ring-𝔽 ∘ A)
-
-  is-set-type-Π-Commutative-Ring-𝔽 : is-set type-Π-Commutative-Ring-𝔽
-  is-set-type-Π-Commutative-Ring-𝔽 =
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  type-Π-Finite-Commutative-Ring : UU (l1 ⊔ l2)
+  type-Π-Finite-Commutative-Ring =
+    type-Π-Commutative-Ring
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  finite-type-Π-Finite-Commutative-Ring : Finite-Type (l1 ⊔ l2)
+  finite-type-Π-Finite-Commutative-Ring =
+    finite-type-Π-Finite-Ring I (finite-ring-Finite-Commutative-Ring ∘ A)
+
+  is-finite-type-Π-Finite-Commutative-Ring :
+    is-finite type-Π-Finite-Commutative-Ring
+  is-finite-type-Π-Finite-Commutative-Ring =
+    is-finite-type-Π-Finite-Ring I (finite-ring-Finite-Commutative-Ring ∘ A)
+
+  is-set-type-Π-Finite-Commutative-Ring : is-set type-Π-Finite-Commutative-Ring
+  is-set-type-Π-Finite-Commutative-Ring =
     is-set-type-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  add-Π-Commutative-Ring-𝔽 :
-    type-Π-Commutative-Ring-𝔽 → type-Π-Commutative-Ring-𝔽 →
-    type-Π-Commutative-Ring-𝔽
-  add-Π-Commutative-Ring-𝔽 =
-    add-Π-Commutative-Ring (type-𝔽 I) (commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  zero-Π-Commutative-Ring-𝔽 : type-Π-Commutative-Ring-𝔽
-  zero-Π-Commutative-Ring-𝔽 =
-    zero-Π-Commutative-Ring (type-𝔽 I) (commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  associative-add-Π-Commutative-Ring-𝔽 :
-    (x y z : type-Π-Commutative-Ring-𝔽) →
-    add-Π-Commutative-Ring-𝔽 (add-Π-Commutative-Ring-𝔽 x y) z ＝
-    add-Π-Commutative-Ring-𝔽 x (add-Π-Commutative-Ring-𝔽 y z)
-  associative-add-Π-Commutative-Ring-𝔽 =
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  add-Π-Finite-Commutative-Ring :
+    type-Π-Finite-Commutative-Ring → type-Π-Finite-Commutative-Ring →
+    type-Π-Finite-Commutative-Ring
+  add-Π-Finite-Commutative-Ring =
+    add-Π-Commutative-Ring
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  zero-Π-Finite-Commutative-Ring : type-Π-Finite-Commutative-Ring
+  zero-Π-Finite-Commutative-Ring =
+    zero-Π-Commutative-Ring
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  associative-add-Π-Finite-Commutative-Ring :
+    (x y z : type-Π-Finite-Commutative-Ring) →
+    add-Π-Finite-Commutative-Ring (add-Π-Finite-Commutative-Ring x y) z ＝
+    add-Π-Finite-Commutative-Ring x (add-Π-Finite-Commutative-Ring y z)
+  associative-add-Π-Finite-Commutative-Ring =
     associative-add-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
 
-  left-unit-law-add-Π-Commutative-Ring-𝔽 :
-    (x : type-Π-Commutative-Ring-𝔽) →
-    add-Π-Commutative-Ring-𝔽 zero-Π-Commutative-Ring-𝔽 x ＝ x
-  left-unit-law-add-Π-Commutative-Ring-𝔽 =
+  left-unit-law-add-Π-Finite-Commutative-Ring :
+    (x : type-Π-Finite-Commutative-Ring) →
+    add-Π-Finite-Commutative-Ring zero-Π-Finite-Commutative-Ring x ＝ x
+  left-unit-law-add-Π-Finite-Commutative-Ring =
     left-unit-law-add-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
 
-  right-unit-law-add-Π-Commutative-Ring-𝔽 :
-    (x : type-Π-Commutative-Ring-𝔽) →
-    add-Π-Commutative-Ring-𝔽 x zero-Π-Commutative-Ring-𝔽 ＝ x
-  right-unit-law-add-Π-Commutative-Ring-𝔽 =
+  right-unit-law-add-Π-Finite-Commutative-Ring :
+    (x : type-Π-Finite-Commutative-Ring) →
+    add-Π-Finite-Commutative-Ring x zero-Π-Finite-Commutative-Ring ＝ x
+  right-unit-law-add-Π-Finite-Commutative-Ring =
     right-unit-law-add-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
 
-  commutative-add-Π-Commutative-Ring-𝔽 :
-    (x y : type-Π-Commutative-Ring-𝔽) →
-    add-Π-Commutative-Ring-𝔽 x y ＝ add-Π-Commutative-Ring-𝔽 y x
-  commutative-add-Π-Commutative-Ring-𝔽 =
+  commutative-add-Π-Finite-Commutative-Ring :
+    (x y : type-Π-Finite-Commutative-Ring) →
+    add-Π-Finite-Commutative-Ring x y ＝ add-Π-Finite-Commutative-Ring y x
+  commutative-add-Π-Finite-Commutative-Ring =
     commutative-add-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  mul-Π-Commutative-Ring-𝔽 :
-    type-Π-Commutative-Ring-𝔽 → type-Π-Commutative-Ring-𝔽 →
-    type-Π-Commutative-Ring-𝔽
-  mul-Π-Commutative-Ring-𝔽 =
-    mul-Π-Commutative-Ring (type-𝔽 I) (commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  one-Π-Commutative-Ring-𝔽 : type-Π-Commutative-Ring-𝔽
-  one-Π-Commutative-Ring-𝔽 =
-    one-Π-Commutative-Ring (type-𝔽 I) (commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  associative-mul-Π-Commutative-Ring-𝔽 :
-    (x y z : type-Π-Commutative-Ring-𝔽) →
-    mul-Π-Commutative-Ring-𝔽 (mul-Π-Commutative-Ring-𝔽 x y) z ＝
-    mul-Π-Commutative-Ring-𝔽 x (mul-Π-Commutative-Ring-𝔽 y z)
-  associative-mul-Π-Commutative-Ring-𝔽 =
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  mul-Π-Finite-Commutative-Ring :
+    type-Π-Finite-Commutative-Ring → type-Π-Finite-Commutative-Ring →
+    type-Π-Finite-Commutative-Ring
+  mul-Π-Finite-Commutative-Ring =
+    mul-Π-Commutative-Ring
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  one-Π-Finite-Commutative-Ring : type-Π-Finite-Commutative-Ring
+  one-Π-Finite-Commutative-Ring =
+    one-Π-Commutative-Ring
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  associative-mul-Π-Finite-Commutative-Ring :
+    (x y z : type-Π-Finite-Commutative-Ring) →
+    mul-Π-Finite-Commutative-Ring (mul-Π-Finite-Commutative-Ring x y) z ＝
+    mul-Π-Finite-Commutative-Ring x (mul-Π-Finite-Commutative-Ring y z)
+  associative-mul-Π-Finite-Commutative-Ring =
     associative-mul-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
 
-  left-unit-law-mul-Π-Commutative-Ring-𝔽 :
-    (x : type-Π-Commutative-Ring-𝔽) →
-    mul-Π-Commutative-Ring-𝔽 one-Π-Commutative-Ring-𝔽 x ＝ x
-  left-unit-law-mul-Π-Commutative-Ring-𝔽 =
+  left-unit-law-mul-Π-Finite-Commutative-Ring :
+    (x : type-Π-Finite-Commutative-Ring) →
+    mul-Π-Finite-Commutative-Ring one-Π-Finite-Commutative-Ring x ＝ x
+  left-unit-law-mul-Π-Finite-Commutative-Ring =
     left-unit-law-mul-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
 
-  right-unit-law-mul-Π-Commutative-Ring-𝔽 :
-    (x : type-Π-Commutative-Ring-𝔽) →
-    mul-Π-Commutative-Ring-𝔽 x one-Π-Commutative-Ring-𝔽 ＝ x
-  right-unit-law-mul-Π-Commutative-Ring-𝔽 =
+  right-unit-law-mul-Π-Finite-Commutative-Ring :
+    (x : type-Π-Finite-Commutative-Ring) →
+    mul-Π-Finite-Commutative-Ring x one-Π-Finite-Commutative-Ring ＝ x
+  right-unit-law-mul-Π-Finite-Commutative-Ring =
     right-unit-law-mul-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  left-distributive-mul-add-Π-Commutative-Ring-𝔽 :
-    (f g h : type-Π-Commutative-Ring-𝔽) →
-    mul-Π-Commutative-Ring-𝔽 f (add-Π-Commutative-Ring-𝔽 g h) ＝
-    add-Π-Commutative-Ring-𝔽
-      ( mul-Π-Commutative-Ring-𝔽 f g)
-      ( mul-Π-Commutative-Ring-𝔽 f h)
-  left-distributive-mul-add-Π-Commutative-Ring-𝔽 =
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  left-distributive-mul-add-Π-Finite-Commutative-Ring :
+    (f g h : type-Π-Finite-Commutative-Ring) →
+    mul-Π-Finite-Commutative-Ring f (add-Π-Finite-Commutative-Ring g h) ＝
+    add-Π-Finite-Commutative-Ring
+      ( mul-Π-Finite-Commutative-Ring f g)
+      ( mul-Π-Finite-Commutative-Ring f h)
+  left-distributive-mul-add-Π-Finite-Commutative-Ring =
     left-distributive-mul-add-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  right-distributive-mul-add-Π-Commutative-Ring-𝔽 :
-    (f g h : type-Π-Commutative-Ring-𝔽) →
-    mul-Π-Commutative-Ring-𝔽 (add-Π-Commutative-Ring-𝔽 f g) h ＝
-    add-Π-Commutative-Ring-𝔽
-      ( mul-Π-Commutative-Ring-𝔽 f h)
-      ( mul-Π-Commutative-Ring-𝔽 g h)
-  right-distributive-mul-add-Π-Commutative-Ring-𝔽 =
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  right-distributive-mul-add-Π-Finite-Commutative-Ring :
+    (f g h : type-Π-Finite-Commutative-Ring) →
+    mul-Π-Finite-Commutative-Ring (add-Π-Finite-Commutative-Ring f g) h ＝
+    add-Π-Finite-Commutative-Ring
+      ( mul-Π-Finite-Commutative-Ring f h)
+      ( mul-Π-Finite-Commutative-Ring g h)
+  right-distributive-mul-add-Π-Finite-Commutative-Ring =
     right-distributive-mul-add-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  left-zero-law-mul-Π-Commutative-Ring-𝔽 :
-    (f : type-Π-Commutative-Ring-𝔽) →
-    mul-Π-Commutative-Ring-𝔽 zero-Π-Commutative-Ring-𝔽 f ＝
-    zero-Π-Commutative-Ring-𝔽
-  left-zero-law-mul-Π-Commutative-Ring-𝔽 =
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  left-zero-law-mul-Π-Finite-Commutative-Ring :
+    (f : type-Π-Finite-Commutative-Ring) →
+    mul-Π-Finite-Commutative-Ring zero-Π-Finite-Commutative-Ring f ＝
+    zero-Π-Finite-Commutative-Ring
+  left-zero-law-mul-Π-Finite-Commutative-Ring =
     left-zero-law-mul-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  right-zero-law-mul-Π-Commutative-Ring-𝔽 :
-    (f : type-Π-Commutative-Ring-𝔽) →
-    mul-Π-Commutative-Ring-𝔽 f zero-Π-Commutative-Ring-𝔽 ＝
-    zero-Π-Commutative-Ring-𝔽
-  right-zero-law-mul-Π-Commutative-Ring-𝔽 =
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  right-zero-law-mul-Π-Finite-Commutative-Ring :
+    (f : type-Π-Finite-Commutative-Ring) →
+    mul-Π-Finite-Commutative-Ring f zero-Π-Finite-Commutative-Ring ＝
+    zero-Π-Finite-Commutative-Ring
+  right-zero-law-mul-Π-Finite-Commutative-Ring =
     right-zero-law-mul-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
 
-  commutative-mul-Π-Commutative-Ring-𝔽 :
-    (f g : type-Π-Commutative-Ring-𝔽) →
-    mul-Π-Commutative-Ring-𝔽 f g ＝ mul-Π-Commutative-Ring-𝔽 g f
-  commutative-mul-Π-Commutative-Ring-𝔽 =
+  commutative-mul-Π-Finite-Commutative-Ring :
+    (f g : type-Π-Finite-Commutative-Ring) →
+    mul-Π-Finite-Commutative-Ring f g ＝ mul-Π-Finite-Commutative-Ring g f
+  commutative-mul-Π-Finite-Commutative-Ring =
     commutative-mul-Π-Commutative-Ring
-      ( type-𝔽 I)
-      ( commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  commutative-ring-Π-Commutative-Ring-𝔽 : Commutative-Ring (l1 ⊔ l2)
-  commutative-ring-Π-Commutative-Ring-𝔽 =
-    Π-Commutative-Ring (type-𝔽 I) (commutative-ring-Commutative-Ring-𝔽 ∘ A)
-
-  Π-Commutative-Ring-𝔽 : Commutative-Ring-𝔽 (l1 ⊔ l2)
-  pr1 Π-Commutative-Ring-𝔽 = finite-ring-Π-Commutative-Ring-𝔽
-  pr2 Π-Commutative-Ring-𝔽 = commutative-mul-Π-Commutative-Ring-𝔽
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  commutative-ring-Π-Finite-Commutative-Ring : Commutative-Ring (l1 ⊔ l2)
+  commutative-ring-Π-Finite-Commutative-Ring =
+    Π-Commutative-Ring
+      ( type-Finite-Type I)
+      ( commutative-ring-Finite-Commutative-Ring ∘ A)
+
+  Π-Finite-Commutative-Ring : Finite-Commutative-Ring (l1 ⊔ l2)
+  pr1 Π-Finite-Commutative-Ring = finite-ring-Π-Finite-Commutative-Ring
+  pr2 Π-Finite-Commutative-Ring = commutative-mul-Π-Finite-Commutative-Ring
 ```