Fix terminology for π-finite types (#1234)

Implements the naming change
- "π-finite" ↦ "untruncated π-finite"
- "truncated π-finite" ↦ "π-finite"

and formalizes the missing results where it is stated that a type is
π-finite, but it is only formalized that it is untruncated π-finite


Co-authored-by: Egbert Rijke <[email protected]>

src/finite-group-theory/finite-groups.lagda.md

@@ -12,6 +12,7 @@ open import elementary-number-theory.natural-numbers
 open import finite-group-theory.finite-monoids
 open import finite-group-theory.finite-semigroups
 
+open import foundation.1-types
 open import foundation.binary-embeddings
 open import foundation.binary-equivalences
 open import foundation.decidable-equality
@@ -30,6 +31,7 @@ open import foundation.sets
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
 
+open import group-theory.category-of-groups
 open import group-theory.commuting-elements-groups
 open import group-theory.groups
 open import group-theory.monoids
@@ -51,6 +53,7 @@ open import univalent-combinatorics.finitely-many-connected-components
 open import univalent-combinatorics.function-types
 open import univalent-combinatorics.pi-finite-types
 open import univalent-combinatorics.standard-finite-types
+open import univalent-combinatorics.untruncated-pi-finite-types
 ```
 
 </details>
@@ -329,10 +332,26 @@ module _
 ```agda
 Group-of-Order : (l : Level) (n : ℕ) → UU (lsuc l)
 Group-of-Order l n = Σ (Group l) (λ G → mere-equiv (Fin n) (type-Group G))
+
+Group-of-Order' : (l : Level) (n : ℕ) → UU (lsuc l)
+Group-of-Order' l n =
+  Σ (Semigroup-of-Order l n) (λ X → is-group-Semigroup (pr1 X))
+
+compute-Group-of-Order :
+  {l : Level} (n : ℕ) → Group-of-Order l n ≃ Group-of-Order' l n
+compute-Group-of-Order n = equiv-right-swap-Σ
 ```
 
 ## Properties
 
+### The type of groups of order `n` is a 1-type
+
+```agda
+is-1-type-Group-of-Order : {l : Level} (n : ℕ) → is-1-type (Group-of-Order l n)
+is-1-type-Group-of-Order n =
+  is-1-type-type-subtype (mere-equiv-Prop (Fin n) ∘ type-Group) is-1-type-Group
+```
+
 ### The type `is-group-Semigroup G` is finite for any semigroup of fixed finite order
 
 ```agda
@@ -384,26 +403,41 @@ is-finite-is-group-Semigroup {l} n G =
                         ( pair n e)
                         ( mul-Semigroup (pr1 G) x (i x))
                         ( pr1 u)))))))
+```
 
-is-π-finite-Group-of-Order :
-  {l : Level} (k n : ℕ) → is-π-finite k (Group-of-Order l n)
-is-π-finite-Group-of-Order {l} k n =
-  is-π-finite-equiv k e
-    ( is-π-finite-Σ k
-      ( is-π-finite-Semigroup-of-Order (succ-ℕ k) n)
+### The type of groups of order `n` is π₁-finite
+
+```agda
+is-untruncated-π-finite-Group-of-Order :
+  {l : Level} (k n : ℕ) → is-untruncated-π-finite k (Group-of-Order l n)
+is-untruncated-π-finite-Group-of-Order {l} k n =
+  is-untruncated-π-finite-equiv k
+    ( compute-Group-of-Order n)
+    ( is-untruncated-π-finite-Σ k
+      ( is-untruncated-π-finite-Semigroup-of-Order (succ-ℕ k) n)
       ( λ X →
-        is-π-finite-is-finite k
+        is-untruncated-π-finite-is-finite k
           ( is-finite-is-group-Semigroup n X)))
-  where
-  e :
-    Group-of-Order l n ≃
-    Σ (Semigroup-of-Order l n) (λ X → is-group-Semigroup (pr1 X))
-  e = equiv-right-swap-Σ
 
+is-π-finite-Group-of-Order :
+  {l : Level} (n : ℕ) → is-π-finite 1 (Group-of-Order l n)
+is-π-finite-Group-of-Order n =
+  is-π-finite-is-untruncated-π-finite 1
+    ( is-1-type-Group-of-Order n)
+    ( is-untruncated-π-finite-Group-of-Order 1 n)
+```
+
+### The number of groups of a given order up to isomorphism
+
+The number of groups of order `n` is listed as
+[A000001](https://oeis.org/A000001) in the [OEIS](literature.oeis.md)
+{{#cite oeis}}.
+
+```agda
 number-of-groups-of-order : ℕ → ℕ
 number-of-groups-of-order n =
   number-of-connected-components
-    ( is-π-finite-Group-of-Order {lzero} zero-ℕ n)
+    ( is-untruncated-π-finite-Group-of-Order {lzero} zero-ℕ n)
 
 mere-equiv-number-of-groups-of-order :
   (n : ℕ) →
@@ -412,7 +446,7 @@ mere-equiv-number-of-groups-of-order :
     ( type-trunc-Set (Group-of-Order lzero n))
 mere-equiv-number-of-groups-of-order n =
   mere-equiv-number-of-connected-components
-    ( is-π-finite-Group-of-Order {lzero} zero-ℕ n)
+    ( is-untruncated-π-finite-Group-of-Order {lzero} zero-ℕ n)
 ```
 
 ### There is a finite number of ways to equip a finite type with the structure of a group
@@ -454,3 +488,7 @@ module _
                     ( is-finite-type-𝔽 X)
                     ( λ x → is-finite-eq-𝔽 X)))))
 ```
+
+## References
+
+{{#bibliography}}

src/finite-group-theory/finite-monoids.lagda.md

@@ -11,6 +11,7 @@ open import elementary-number-theory.natural-numbers
 
 open import finite-group-theory.finite-semigroups
 
+open import foundation.1-types
 open import foundation.decidable-propositions
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
@@ -39,13 +40,16 @@ open import univalent-combinatorics.finite-types
 open import univalent-combinatorics.finitely-many-connected-components
 open import univalent-combinatorics.pi-finite-types
 open import univalent-combinatorics.standard-finite-types
+open import univalent-combinatorics.untruncated-pi-finite-types
 ```
 
 </details>
 
 ## Idea
 
-A finite monoid is a monoid of which the underlying type is finite.
+A {{#concept "finite monoid" Agda=Monoid-𝔽}} is a
+[monoid](group-theory.monoids.md) of which the underlying type is
+[finite](univalent-combinatorics.finite-types.md).
 
 ## Definition
 
@@ -125,6 +129,14 @@ module _
 ```agda
 Monoid-of-Order : (l : Level) (n : ℕ) → UU (lsuc l)
 Monoid-of-Order l n = Σ (Monoid l) (λ M → mere-equiv (Fin n) (type-Monoid M))
+
+Monoid-of-Order' : (l : Level) (n : ℕ) → UU (lsuc l)
+Monoid-of-Order' l n =
+    Σ (Semigroup-of-Order l n) (λ X → is-unital-Semigroup (pr1 X))
+
+compute-Monoid-of-Order :
+  {l : Level} (n : ℕ) → Monoid-of-Order l n ≃ Monoid-of-Order' l n
+compute-Monoid-of-Order n = equiv-right-swap-Σ
 ```
 
 ## Properties
@@ -162,32 +174,59 @@ is-finite-is-unital-Semigroup {l} n X =
                     ( x))))))
 ```
 
-### The type of monoids of order `n` is π-finite
+### The type of monoids of order `n` is a 1-type
 
 ```agda
-is-π-finite-Monoid-of-Order :
-  {l : Level} (k n : ℕ) → is-π-finite k (Monoid-of-Order l n)
-is-π-finite-Monoid-of-Order {l} k n =
-  is-π-finite-equiv k e
-    ( is-π-finite-Σ k
-      ( is-π-finite-Semigroup-of-Order (succ-ℕ k) n)
+is-1-type-Monoid-of-Order' :
+  {l : Level} (n : ℕ) → is-1-type (Monoid-of-Order' l n)
+is-1-type-Monoid-of-Order' n =
+  is-1-type-Σ
+    ( is-1-type-Semigroup-of-Order n)
+    ( λ G →
+      is-1-type-is-set (is-set-is-finite (is-finite-is-unital-Semigroup n G)))
+
+is-1-type-Monoid-of-Order :
+  {l : Level} (n : ℕ) → is-1-type (Monoid-of-Order l n)
+is-1-type-Monoid-of-Order {l} n =
+  is-1-type-equiv
+    ( Monoid-of-Order' l n)
+    ( compute-Monoid-of-Order n)
+    ( is-1-type-Monoid-of-Order' n)
+```
+
+### The type of monoids of order `n` is π₁-finite
+
+```agda
+is-untruncated-π-finite-Monoid-of-Order :
+  {l : Level} (k n : ℕ) → is-untruncated-π-finite k (Monoid-of-Order l n)
+is-untruncated-π-finite-Monoid-of-Order {l} k n =
+  is-untruncated-π-finite-equiv k
+    ( compute-Monoid-of-Order n)
+    ( is-untruncated-π-finite-Σ k
+      ( is-untruncated-π-finite-Semigroup-of-Order (succ-ℕ k) n)
       ( λ X →
-        is-π-finite-is-finite k
+        is-untruncated-π-finite-is-finite k
           ( is-finite-is-unital-Semigroup n X)))
-  where
-  e :
-    Monoid-of-Order l n ≃
-    Σ (Semigroup-of-Order l n) (λ X → is-unital-Semigroup (pr1 X))
-  e = equiv-right-swap-Σ
+
+is-π-finite-Monoid-of-Order :
+  {l : Level} (n : ℕ) → is-π-finite 1 (Monoid-of-Order l n)
+is-π-finite-Monoid-of-Order n =
+  is-π-finite-is-untruncated-π-finite 1
+    ( is-1-type-Monoid-of-Order n)
+    ( is-untruncated-π-finite-Monoid-of-Order 1 n)
 ```
 
-### The function that returns for any `n` the number of monoids of order `n` up to isomorphism
+### The number of monoids of a given order up to isomorphism
+
+The number of monoids of order `n` is listed as
+[A058129](https://oeis.org/A058129) in the [OEIS](literature.oeis.md)
+{{#cite oeis}}.
 
 ```agda
 number-of-monoids-of-order : ℕ → ℕ
 number-of-monoids-of-order n =
   number-of-connected-components
-    ( is-π-finite-Monoid-of-Order {lzero} zero-ℕ n)
+    ( is-untruncated-π-finite-Monoid-of-Order {lzero} zero-ℕ n)
 
 mere-equiv-number-of-monoids-of-order :
   (n : ℕ) →
@@ -196,7 +235,7 @@ mere-equiv-number-of-monoids-of-order :
     ( type-trunc-Set (Monoid-of-Order lzero n))
 mere-equiv-number-of-monoids-of-order n =
   mere-equiv-number-of-connected-components
-    ( is-π-finite-Monoid-of-Order {lzero} zero-ℕ n)
+    ( is-untruncated-π-finite-Monoid-of-Order {lzero} zero-ℕ n)
 ```
 
 ### For any finite semigroup `G`, being unital is a property
@@ -251,3 +290,7 @@ is-finite-structure-monoid-𝔽 X =
     ( is-finite-structure-semigroup-𝔽 X)
     ( λ m → is-finite-is-unital-Semigroup-𝔽 (X , m))
 ```
+
+## References
+
+{{#bibliography}}