diff --git a/src/finite-group-theory/finite-groups.lagda.md b/src/finite-group-theory/finite-groups.lagda.md
index cf7d3d5663..63e90d8c14 100644
--- a/src/finite-group-theory/finite-groups.lagda.md
+++ b/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}}
diff --git a/src/finite-group-theory/finite-monoids.lagda.md b/src/finite-group-theory/finite-monoids.lagda.md
index d896effcbd..cc1ccf8366 100644
--- a/src/finite-group-theory/finite-monoids.lagda.md
+++ b/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}}
diff --git a/src/finite-group-theory/finite-semigroups.lagda.md b/src/finite-group-theory/finite-semigroups.lagda.md
index 5c6c76c8ba..a44eb7a404 100644
--- a/src/finite-group-theory/finite-semigroups.lagda.md
+++ b/src/finite-group-theory/finite-semigroups.lagda.md
@@ -9,6 +9,7 @@ module finite-group-theory.finite-semigroups where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.1-types
 open import foundation.decidable-propositions
 open import foundation.equivalences
 open import foundation.function-types
@@ -18,9 +19,11 @@ open import foundation.mere-equivalences
 open import foundation.propositions
 open import foundation.set-truncations
 open import foundation.sets
+open import foundation.subtypes
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
 
+open import group-theory.category-of-semigroups
 open import group-theory.semigroups
 
 open import univalent-combinatorics.dependent-function-types
@@ -31,6 +34,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>
@@ -129,6 +133,38 @@ Semigroup-of-Order l n =
 
 ## Properties
 
+### The two definitions of semigroups of order `n` agree
+
+```agda
+compute-Semigroup-of-Order :
+  {l : Level} (n : ℕ) → Semigroup-of-Order l n ≃ Semigroup-of-Order' l n
+compute-Semigroup-of-Order {l} n =
+  ( equiv-Σ
+    ( has-associative-mul ∘ type-UU-Fin n)
+    ( ( right-unit-law-Σ-is-contr
+        ( λ X →
+          is-proof-irrelevant-is-prop
+            ( is-prop-is-set _)
+            ( is-set-is-finite (is-finite-has-cardinality n (pr2 X))))) ∘e
+      ( equiv-right-swap-Σ))
+    ( λ X → id-equiv)) ∘e
+  ( equiv-right-swap-Σ
+    { A = Set l}
+    { B = has-associative-mul-Set}
+    { C = mere-equiv (Fin n) ∘ type-Set})
+```
+
+### The type of semigroups of order `n` is a 1-type
+
+```agda
+is-1-type-Semigroup-of-Order :
+  {l : Level} (n : ℕ) → is-1-type (Semigroup-of-Order l n)
+is-1-type-Semigroup-of-Order n =
+  is-1-type-type-subtype
+    ( mere-equiv-Prop (Fin n) ∘ type-Semigroup)
+    ( is-1-type-Semigroup)
+```
+
 ### If `X` is finite, then there are finitely many associative operations on `X`
 
 ```agda
@@ -147,57 +183,54 @@ is-finite-has-associative-mul H =
                   is-finite-eq (has-decidable-equality-is-finite H)))))
 ```
 
-### The type of semigroups of order `n` is π-finite
+### The type of semigroups of order `n` is π₁-finite
 
 ```agda
-is-π-finite-Semigroup-of-Order' :
-  {l : Level} (k n : ℕ) → is-π-finite k (Semigroup-of-Order' l n)
-is-π-finite-Semigroup-of-Order' k n =
-  is-π-finite-Σ k
-    ( is-π-finite-UU-Fin (succ-ℕ k) n)
+is-untruncated-π-finite-Semigroup-of-Order' :
+  {l : Level} (k n : ℕ) → is-untruncated-π-finite k (Semigroup-of-Order' l n)
+is-untruncated-π-finite-Semigroup-of-Order' k n =
+  is-untruncated-π-finite-Σ k
+    ( is-untruncated-π-finite-UU-Fin (succ-ℕ k) n)
     ( λ x →
-      is-π-finite-is-finite k
+      is-untruncated-π-finite-is-finite k
         ( is-finite-has-associative-mul
           ( is-finite-type-UU-Fin n x)))
 
+is-untruncated-π-finite-Semigroup-of-Order :
+  {l : Level} (k n : ℕ) → is-untruncated-π-finite k (Semigroup-of-Order l n)
+is-untruncated-π-finite-Semigroup-of-Order k n =
+  is-untruncated-π-finite-equiv k
+    ( compute-Semigroup-of-Order n)
+    ( is-untruncated-π-finite-Semigroup-of-Order' k n)
+
 is-π-finite-Semigroup-of-Order :
-  {l : Level} (k n : ℕ) → is-π-finite k (Semigroup-of-Order l n)
-is-π-finite-Semigroup-of-Order {l} k n =
-  is-π-finite-equiv k e
-    ( is-π-finite-Semigroup-of-Order' k n)
-  where
-  e : Semigroup-of-Order l n ≃ Semigroup-of-Order' l n
-  e = ( equiv-Σ
-        ( has-associative-mul ∘ type-UU-Fin n)
-        ( ( right-unit-law-Σ-is-contr
-            ( λ X →
-              is-proof-irrelevant-is-prop
-                ( is-prop-is-set _)
-                ( is-set-is-finite (is-finite-has-cardinality n (pr2 X))))) ∘e
-          ( equiv-right-swap-Σ))
-        ( λ X → id-equiv)) ∘e
-      ( equiv-right-swap-Σ
-        { A = Set l}
-        { B = has-associative-mul-Set}
-        { C = mere-equiv (Fin n) ∘ type-Set})
+  {l : Level} (n : ℕ) → is-π-finite 1 (Semigroup-of-Order l n)
+is-π-finite-Semigroup-of-Order {l} n =
+  is-π-finite-is-untruncated-π-finite 1
+    ( is-1-type-Semigroup-of-Order n)
+    ( is-untruncated-π-finite-Semigroup-of-Order 1 n)
 ```
 
-### The function that returns for each `n` the number of semigroups of order `n` up to isomorphism
+### The number of semigroups of a given order up to isomorphism
+
+The number of semigroups of order `n` is listed as
+[A027851](https://oeis.org/A027851) in the [OEIS](literature.oeis.md)
+{{#cite oeis}}.
 
 ```agda
-number-of-semi-groups-of-order : ℕ → ℕ
-number-of-semi-groups-of-order n =
+number-of-semigroups-of-order : ℕ → ℕ
+number-of-semigroups-of-order n =
   number-of-connected-components
-    ( is-π-finite-Semigroup-of-Order {lzero} zero-ℕ n)
+    ( is-untruncated-π-finite-Semigroup-of-Order {lzero} zero-ℕ n)
 
-mere-equiv-number-of-semi-groups-of-order :
+mere-equiv-number-of-semigroups-of-order :
   (n : ℕ) →
   mere-equiv
-    ( Fin (number-of-semi-groups-of-order n))
+    ( Fin (number-of-semigroups-of-order n))
     ( type-trunc-Set (Semigroup-of-Order lzero n))
-mere-equiv-number-of-semi-groups-of-order n =
+mere-equiv-number-of-semigroups-of-order n =
   mere-equiv-number-of-connected-components
-    ( is-π-finite-Semigroup-of-Order {lzero} zero-ℕ n)
+    ( is-untruncated-π-finite-Semigroup-of-Order {lzero} zero-ℕ n)
 ```
 
 ### There is a finite number of ways to equip a finite type with the structure of a semigroup
@@ -235,3 +268,7 @@ is-finite-structure-semigroup-𝔽 X =
                       ( m (m x y) z)
                       ( m x (m y z)))))))
 ```
+
+## References
+
+{{#bibliography}}
diff --git a/src/foundation/1-types.lagda.md b/src/foundation/1-types.lagda.md
index 0e05ba4da8..cdce9dfe87 100644
--- a/src/foundation/1-types.lagda.md
+++ b/src/foundation/1-types.lagda.md
@@ -181,3 +181,22 @@ module _
   eq-equiv-1-Type : (Y : 1-Type l) → type-equiv-1-Type Y → X ＝ Y
   eq-equiv-1-Type Y = eq-equiv-subuniverse is-1-type-Prop
 ```
+
+### 1-types are `k+3`-truncated for any `k`
+
+```agda
+is-trunc-is-1-type :
+  {l : Level} (k : 𝕋) {A : UU l} →
+  is-1-type A →
+  is-trunc (succ-𝕋 (succ-𝕋 (succ-𝕋 k))) A
+is-trunc-is-1-type neg-two-𝕋 is-1-type-A = is-1-type-A
+is-trunc-is-1-type (succ-𝕋 k) is-1-type-A =
+  is-trunc-succ-is-trunc
+    ( succ-𝕋 (succ-𝕋 (succ-𝕋 k)))
+    ( is-trunc-is-1-type k is-1-type-A)
+
+1-type-Truncated-Type :
+  {l : Level} (k : 𝕋) → 1-Type l → Truncated-Type l (succ-𝕋 (succ-𝕋 (succ-𝕋 k)))
+pr1 (1-type-Truncated-Type k A) = type-1-Type A
+pr2 (1-type-Truncated-Type k A) = is-trunc-is-1-type k (is-1-type-type-1-Type A)
+```
diff --git a/src/foundation/unordered-tuples-of-types.lagda.md b/src/foundation/unordered-tuples-of-types.lagda.md
index a037d4d4cc..245b0763bd 100644
--- a/src/foundation/unordered-tuples-of-types.lagda.md
+++ b/src/foundation/unordered-tuples-of-types.lagda.md
@@ -27,7 +27,8 @@ open import univalent-combinatorics.finite-types
 
 ## Idea
 
-An unordered tuple of types is an unordered tuple of elements in a universe
+An {{#concept "unordered tuple of types" Agda=unordered-tuple-types}} is an
+[unordered tuple](foundation.unordered-tuples.md) of elements in a universe.
 
 ## Definitions
 
diff --git a/src/foundation/unordered-tuples.lagda.md b/src/foundation/unordered-tuples.lagda.md
index 03fa22fab0..ea8ca7e989 100644
--- a/src/foundation/unordered-tuples.lagda.md
+++ b/src/foundation/unordered-tuples.lagda.md
@@ -9,12 +9,15 @@ module foundation.unordered-tuples where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.1-types
 open import foundation.decidable-equality
 open import foundation.dependent-pair-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopy-induction
 open import foundation.postcomposition-functions
 open import foundation.structure-identity-principle
+open import foundation.truncated-types
+open import foundation.truncation-levels
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
@@ -36,8 +39,11 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-An **unordered `n`-tuple** of elements of a type `A` consists of an `n`-element
-set `X` equipped with a map `X → A`.
+An
+{{#concept "unordered `n`-tuple" WDID=Q43851442 WD="unordered 𝑛-tuple" Agda=unordered-tuple}}
+of elements of a type `A` consists of an
+[`n`-element set](univalent-combinatorics.finite-types.md) `X`
+[equipped](foundation.structure.md) with a map `X → A`.
 
 ## Definition
 
@@ -173,6 +179,28 @@ module _
     is-retraction-map-inv-is-equiv (is-equiv-Eq-eq-unordered-tuple x y)
 ```
 
+### The type of unordered tuples in a truncated type is truncated
+
+```agda
+is-trunc-succ-succ-succ-unordered-tuple :
+  {l : Level} (k : 𝕋) (n : ℕ) {A : UU l} →
+  is-trunc (succ-𝕋 (succ-𝕋 (succ-𝕋 k))) A →
+  is-trunc (succ-𝕋 (succ-𝕋 (succ-𝕋 k))) (unordered-tuple n A)
+is-trunc-succ-succ-succ-unordered-tuple k n H =
+  is-trunc-Σ
+    ( is-trunc-is-1-type k (is-1-type-UU-Fin n))
+    ( λ X → is-trunc-function-type (succ-𝕋 (succ-𝕋 (succ-𝕋 k))) H)
+```
+
+### The type of unordered tuples in a 1-type is a 1-type
+
+```agda
+is-1-type-unordered-tuple :
+  {l : Level} (n : ℕ) {A : UU l} →
+  is-1-type A → is-1-type (unordered-tuple n A)
+is-1-type-unordered-tuple = is-trunc-succ-succ-succ-unordered-tuple neg-two-𝕋
+```
+
 ### Functoriality of unordered tuples
 
 ```agda
diff --git a/src/group-theory/category-of-groups.lagda.md b/src/group-theory/category-of-groups.lagda.md
index e543101e66..5b7a7ec268 100644
--- a/src/group-theory/category-of-groups.lagda.md
+++ b/src/group-theory/category-of-groups.lagda.md
@@ -10,6 +10,7 @@ module group-theory.category-of-groups where
 open import category-theory.categories
 open import category-theory.large-categories
 
+open import foundation.1-types
 open import foundation.equivalences
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
@@ -22,7 +23,7 @@ open import group-theory.precategory-of-groups
 
 </details>
 
-## Definition
+## Definitions
 
 ```agda
 is-large-category-Group :
@@ -40,3 +41,12 @@ is-large-category-Large-Category Group-Large-Category = is-large-category-Group
 Group-Category : (l : Level) → Category (lsuc l) l
 Group-Category = category-Large-Category Group-Large-Category
 ```
+
+## Corollaries
+
+### The type of groups is a 1-type
+
+```agda
+is-1-type-Group : {l : Level} → is-1-type (Group l)
+is-1-type-Group {l} = is-1-type-obj-Category (Group-Category l)
+```
diff --git a/src/group-theory/category-of-semigroups.lagda.md b/src/group-theory/category-of-semigroups.lagda.md
index 997979a69e..a610b13437 100644
--- a/src/group-theory/category-of-semigroups.lagda.md
+++ b/src/group-theory/category-of-semigroups.lagda.md
@@ -10,6 +10,7 @@ module group-theory.category-of-semigroups where
 open import category-theory.categories
 open import category-theory.large-categories
 
+open import foundation.1-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.fundamental-theorem-of-identity-types
@@ -60,3 +61,12 @@ is-large-category-Large-Category Semigroup-Large-Category =
 Semigroup-Category : (l : Level) → Category (lsuc l) l
 Semigroup-Category = category-Large-Category Semigroup-Large-Category
 ```
+
+## Corollaries
+
+### The type of semigroups is a 1-type
+
+```agda
+is-1-type-Semigroup : {l : Level} → is-1-type (Semigroup l)
+is-1-type-Semigroup {l} = is-1-type-obj-Category (Semigroup-Category l)
+```
diff --git a/src/group-theory/commutative-monoids.lagda.md b/src/group-theory/commutative-monoids.lagda.md
index e48be716ac..89b8b3f6aa 100644
--- a/src/group-theory/commutative-monoids.lagda.md
+++ b/src/group-theory/commutative-monoids.lagda.md
@@ -25,8 +25,9 @@ open import group-theory.semigroups
 
 ## Idea
 
-A {{#concept "commutative monoid" Agda=Commutative-Monoid}} is a
-[monoid](group-theory.monoids.md) `M` in which `xy = yx` holds for all
+A
+{{#concept "commutative monoid" WDID=Q19934355 WD="commutative monoid" Agda=Commutative-Monoid}}
+is a [monoid](group-theory.monoids.md) `M` in which `xy = yx` holds for all
 `x y : M`.
 
 ## Definitions
diff --git a/src/group-theory/monoids.lagda.md b/src/group-theory/monoids.lagda.md
index 8f439ce68f..1e76dbc225 100644
--- a/src/group-theory/monoids.lagda.md
+++ b/src/group-theory/monoids.lagda.md
@@ -26,7 +26,8 @@ open import structured-types.wild-monoids
 
 ## Idea
 
-**Monoids** are [unital](foundation.unital-binary-operations.md)
+{{#concept "Monoids" WDID=Q208237 WD="monoid" Agda=Monoid}} are
+[unital](foundation.unital-binary-operations.md)
 [semigroups](group-theory.semigroups.md).
 
 ## Definition
diff --git a/src/group-theory/semigroups.lagda.md b/src/group-theory/semigroups.lagda.md
index be720c9094..4709573fcf 100644
--- a/src/group-theory/semigroups.lagda.md
+++ b/src/group-theory/semigroups.lagda.md
@@ -19,15 +19,16 @@ open import foundation.universe-levels
 
 ## Idea
 
-**Semigroups** are [sets](foundation-core.sets.md) equipped with an associative
-binary operation.
+{{#concept "Semigroups" WDID=Q207348 WD="semigroup" Agda=Semigroup}} are
+[sets](foundation-core.sets.md) [equipped](foundation.structure.md) with an
+associative binary operation.
 
 ## Definitions
 
 ```agda
 has-associative-mul : {l : Level} (X : UU l) → UU l
 has-associative-mul X =
-  Σ (X → X → X) (λ μ → (x y z : X) → Id (μ (μ x y) z) (μ x (μ y z)))
+  Σ (X → X → X) (λ μ → (x y z : X) → μ (μ x y) z ＝ μ x (μ y z))
 
 has-associative-mul-Set :
   {l : Level} (X : Set l) → UU l
diff --git a/src/literature/oeis.lagda.md b/src/literature/oeis.lagda.md
index 31a52f6beb..abb585cf88 100644
--- a/src/literature/oeis.lagda.md
+++ b/src/literature/oeis.lagda.md
@@ -175,6 +175,13 @@ open import elementary-number-theory.collatz-bijection using
   ( map-collatz-bijection)
 ```
 
+### [A027851](https://oeis.org/A027851) The number of semigroups of order `n` up to isomorphism
+
+```agda
+open import finite-group-theory.finite-semigroups using
+  ( number-of-semigroups-of-order)
+```
+
 ### [A046859](https://oeis.org/A046859) The main diagonal of the Ackermann–Péter function
 
 ```agda
@@ -182,6 +189,13 @@ open import elementary-number-theory.ackermann-function using
   ( simplified-ackermann-ℕ)
 ```
 
+### [A058129](https://oeis.org/A058129) The number of monoids of order `n` up to isomorphism
+
+```agda
+open import finite-group-theory.finite-monoids using
+  ( number-of-monoids-of-order)
+```
+
 ## References
 
 {{#bibliography}}
diff --git a/src/univalent-combinatorics.lagda.md b/src/univalent-combinatorics.lagda.md
index ebced9c79d..afd6a44b8c 100644
--- a/src/univalent-combinatorics.lagda.md
+++ b/src/univalent-combinatorics.lagda.md
@@ -15,9 +15,10 @@ the isomorphic objects are identified by the univalence axiom. Univalence can
 therefore help with counting finite structures up to isomorphism. The main piece
 of machinery that helps in this task is the general notion of π-finiteness. A
 level `k` π-finite type is a type that has finitely many connected components,
-such that all its homotopy groups up to level `k` are finite. The π-finite types
-enjoy useful closure properties, such as closedness under Σ, cartesian products,
-coproducts, and closedness under Π under a mild condition.
+such that all its homotopy groups up to level `k` are finite and all its
+homotopy groups above level `k` are trivial. The π-finite types enjoy useful
+closure properties, such as closedness under Σ, cartesian products, coproducts,
+and closedness under Π under a mild condition {{#cite Anel24}}.
 
 ## Modules in the univalent combinatorics namespace
 
@@ -108,7 +109,6 @@ open import univalent-combinatorics.sums-of-natural-numbers public
 open import univalent-combinatorics.surjective-maps public
 open import univalent-combinatorics.symmetric-difference public
 open import univalent-combinatorics.trivial-sigma-decompositions public
-open import univalent-combinatorics.truncated-pi-finite-types public
 open import univalent-combinatorics.type-duality public
 open import univalent-combinatorics.unbounded-pi-finite-types public
 open import univalent-combinatorics.unions-subtypes public
@@ -116,4 +116,9 @@ open import univalent-combinatorics.universal-property-standard-finite-types pub
 open import univalent-combinatorics.unlabeled-partitions public
 open import univalent-combinatorics.unlabeled-rooted-trees public
 open import univalent-combinatorics.unlabeled-trees public
+open import univalent-combinatorics.untruncated-pi-finite-types public
 ```
+
+## References
+
+{{#bibliography}}
diff --git a/src/univalent-combinatorics/latin-squares.lagda.md b/src/univalent-combinatorics/latin-squares.lagda.md
index 4ea5cc9d39..228092c29d 100644
--- a/src/univalent-combinatorics/latin-squares.lagda.md
+++ b/src/univalent-combinatorics/latin-squares.lagda.md
@@ -17,14 +17,15 @@ open import foundation.universe-levels
 
 ## Idea
 
-Latin squares are multiplication tables in which every element appears in every
-row and in every column exactly once. Latin squares are considered to be the
-same if they are isotopic. We therefore define the type of all Latin squares to
-be the type of all inhabited types A, B, and C, equipped with a binary
-equivalence f : A → B → C. The groupoid of main classes of latin squares is
-defined in `main-classes-of-latin-squares`.
+{{#concept "Latin squares" WDID=Q679367 WD="Latin square" Agda=Latin-Square}}
+are multiplication tables in which every element appears in every row and in
+every column exactly once. Latin squares are considered to be the same if they
+are [isotopic](univalent-combinatorics.isotopies-latin-squares.md). We therefore
+define the type of all Latin squares to be the type of all
+[inhabited](foundation.inhabited-types.md) types `A`, `B`, and `C`, equipped
+with a [binary equivalence](foundation.binary-equivalences.md) `f : A → B → C`.
 
-## Definition
+## Definitions
 
 ```agda
 Latin-Square : (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
@@ -73,3 +74,9 @@ module _
     is-binary-equiv mul-Latin-Square
   is-binary-equiv-mul-Latin-Square = pr2 (pr2 (pr2 (pr2 L)))
 ```
+
+## See also
+
+- The [groupoid](foundation.1-types.md) of main classes of latin squares is
+  defined in
+  [`univalent-combinatorics.main-classes-of-latin-squares`](univalent-combinatorics.main-classes-of-latin-squares.md).
diff --git a/src/univalent-combinatorics/main-classes-of-latin-hypercubes.lagda.md b/src/univalent-combinatorics/main-classes-of-latin-hypercubes.lagda.md
index dee4973e2e..e9ed9c79a0 100644
--- a/src/univalent-combinatorics/main-classes-of-latin-hypercubes.lagda.md
+++ b/src/univalent-combinatorics/main-classes-of-latin-hypercubes.lagda.md
@@ -9,6 +9,7 @@ module univalent-combinatorics.main-classes-of-latin-hypercubes where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.1-types
 open import foundation.contractible-types
 open import foundation.decidable-propositions
 open import foundation.dependent-pair-types
@@ -25,11 +26,14 @@ open import univalent-combinatorics.dependent-function-types
 open import univalent-combinatorics.finite-types
 open import univalent-combinatorics.pi-finite-types
 open import univalent-combinatorics.standard-finite-types
+open import univalent-combinatorics.untruncated-pi-finite-types
 ```
 
 </details>
 
-## Definition
+## Definitions
+
+### The type of main classes of Latin hypercubes
 
 ```agda
 Main-Class-Latin-Hypercube : (l1 l2 : Level) (n : ℕ) → UU (lsuc l1 ⊔ lsuc l2)
@@ -54,7 +58,7 @@ Main-Class-Latin-Hypercube l1 l2 n =
                       ( a))))))
 ```
 
-### The groupoid of main classes of Latin hypercubes of fixed finite order
+### The type of main classes of Latin hypercubes of fixed finite order
 
 ```agda
 Main-Class-Latin-Hypercube-of-Order : (n m : ℕ) → UU (lsuc lzero)
@@ -84,24 +88,42 @@ Main-Class-Latin-Hypercube-of-Order n m =
 
 ## Properties
 
-### The groupoid of main classes of Latin hypercubes of finite order is π-finite
+### The type of main classes of Latin hypercubes of fixed finite order is a groupoid
 
 ```agda
-is-π-finite-Main-Class-Latin-Hypercube-of-Order :
-  (k n m : ℕ) → is-π-finite k (Main-Class-Latin-Hypercube-of-Order n m)
-is-π-finite-Main-Class-Latin-Hypercube-of-Order k n m =
-  is-π-finite-Σ k
-    ( is-π-finite-Σ
+is-1-type-Main-Class-Latin-Hypercube-of-Order :
+  (n m : ℕ) → is-1-type (Main-Class-Latin-Hypercube-of-Order n m)
+is-1-type-Main-Class-Latin-Hypercube-of-Order n m =
+  is-1-type-Σ
+    ( is-1-type-unordered-tuple (succ-ℕ n) (is-1-type-UU-Fin m))
+    ( λ A →
+      is-1-type-Σ
+        ( is-1-type-function-type (is-1-type-is-set is-set-Decidable-Prop))
+        ( λ R →
+          is-1-type-Π
+            ( λ i →
+              is-1-type-Π (λ f → is-1-type-is-prop is-property-is-contr))))
+```
+
+### The groupoid of main classes of Latin hypercubes of finite order is unbounded π-finite
+
+```agda
+is-untruncated-π-finite-Main-Class-Latin-Hypercube-of-Order :
+  (k n m : ℕ) →
+  is-untruncated-π-finite k (Main-Class-Latin-Hypercube-of-Order n m)
+is-untruncated-π-finite-Main-Class-Latin-Hypercube-of-Order k n m =
+  is-untruncated-π-finite-Σ k
+    ( is-untruncated-π-finite-Σ
       ( succ-ℕ k)
-      ( is-π-finite-UU-Fin (succ-ℕ (succ-ℕ k)) (succ-ℕ n))
+      ( is-untruncated-π-finite-UU-Fin (succ-ℕ (succ-ℕ k)) (succ-ℕ n))
       ( λ X →
-        is-π-finite-Π
+        is-untruncated-π-finite-Π
           ( succ-ℕ k)
           ( is-finite-type-UU-Fin (succ-ℕ n) X)
-          ( λ i → is-π-finite-UU-Fin (succ-ℕ k) m)))
+          ( λ i → is-untruncated-π-finite-UU-Fin (succ-ℕ k) m)))
     ( λ A →
-      is-π-finite-Σ k
-        ( is-π-finite-is-finite
+      is-untruncated-π-finite-Σ k
+        ( is-untruncated-π-finite-is-finite
           ( succ-ℕ k)
           ( is-finite-Π
             ( is-finite-Π
@@ -113,7 +135,7 @@ is-π-finite-Main-Class-Latin-Hypercube-of-Order k n m =
                   ( element-unordered-tuple (succ-ℕ n) A i)))
             ( λ f → is-finite-Decidable-Prop)))
         ( λ R →
-          is-π-finite-is-finite k
+          is-untruncated-π-finite-is-finite k
             ( is-finite-Π
               ( is-finite-type-UU-Fin
                 ( succ-ℕ n)
@@ -145,13 +167,24 @@ is-π-finite-Main-Class-Latin-Hypercube-of-Order k n m =
                             ( element-unordered-tuple (succ-ℕ n) A i)))))))))
 ```
 
+### The groupoid of main classes of Latin hypercubes of finite order is π₁-finite
+
+```agda
+is-π-finite-Main-Class-Latin-Hypercube-of-Order :
+  (n m : ℕ) → is-π-finite 1 (Main-Class-Latin-Hypercube-of-Order n m)
+is-π-finite-Main-Class-Latin-Hypercube-of-Order n m =
+  is-π-finite-is-untruncated-π-finite 1
+    ( is-1-type-Main-Class-Latin-Hypercube-of-Order n m)
+    ( is-untruncated-π-finite-Main-Class-Latin-Hypercube-of-Order 1 n m)
+```
+
 ### The sequence of main classes of Latin hypercubes of fixed finite order
 
 ```agda
 number-of-main-classes-of-Latin-hypercubes-of-order : ℕ → ℕ → ℕ
 number-of-main-classes-of-Latin-hypercubes-of-order n m =
   number-of-elements-is-finite
-    ( is-π-finite-Main-Class-Latin-Hypercube-of-Order 0 n m)
+    ( is-untruncated-π-finite-Main-Class-Latin-Hypercube-of-Order 0 n m)
 
 mere-equiv-number-of-main-classes-of-Latin-hypercubes-of-order :
   (n m : ℕ) →
@@ -161,5 +194,5 @@ mere-equiv-number-of-main-classes-of-Latin-hypercubes-of-order :
       ( Main-Class-Latin-Hypercube-of-Order n m))
 mere-equiv-number-of-main-classes-of-Latin-hypercubes-of-order n m =
   mere-equiv-is-finite
-    ( is-π-finite-Main-Class-Latin-Hypercube-of-Order 0 n m)
+    ( is-untruncated-π-finite-Main-Class-Latin-Hypercube-of-Order 0 n m)
 ```
diff --git a/src/univalent-combinatorics/main-classes-of-latin-squares.lagda.md b/src/univalent-combinatorics/main-classes-of-latin-squares.lagda.md
index 11839954d6..0f3d9410e3 100644
--- a/src/univalent-combinatorics/main-classes-of-latin-squares.lagda.md
+++ b/src/univalent-combinatorics/main-classes-of-latin-squares.lagda.md
@@ -9,6 +9,7 @@ module univalent-combinatorics.main-classes-of-latin-squares where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.1-types
 open import foundation.mere-equivalences
 open import foundation.set-truncations
 open import foundation.universe-levels
@@ -16,14 +17,18 @@ open import foundation.universe-levels
 open import univalent-combinatorics.main-classes-of-latin-hypercubes
 open import univalent-combinatorics.pi-finite-types
 open import univalent-combinatorics.standard-finite-types
+open import univalent-combinatorics.untruncated-pi-finite-types
 ```
 
 </details>
 
 ## Idea
 
-The groupoid of main classes of latin squares consists of unordered triples of
-inhabited types equipped with a ternary 1-1 correspondence.
+The [groupoid](foundation.1-types.md) of
+{{#concept "main classes of latin squares" Agda=Main-Class-Latin-Squares}}
+consists of [unordered triples](foundation.unordered-tuples.md) of
+[inhabited](foundation.inhabited-types.md) types
+[equipped](foundation.structure.md) with a ternary 1-1 correspondence.
 
 ## Definition
 
@@ -44,13 +49,27 @@ Main-Class-Latin-Square-of-Order m =
 
 ## Properties
 
-### The groupoid of main classes of latin squares of fixed order is π-finite
+### The groupoid of main classes of latin squares of fixed order is a groupoid
 
 ```agda
+is-1-type-Main-Class-Latin-Square-of-Order :
+  (m : ℕ) → is-1-type (Main-Class-Latin-Square-of-Order m)
+is-1-type-Main-Class-Latin-Square-of-Order =
+  is-1-type-Main-Class-Latin-Hypercube-of-Order 2
+```
+
+### The groupoid of main classes of latin squares of fixed order is π₁-finite
+
+```agda
+is-untruncated-π-finite-Main-Class-Latin-Square-of-Order :
+  (k m : ℕ) → is-untruncated-π-finite k (Main-Class-Latin-Square-of-Order m)
+is-untruncated-π-finite-Main-Class-Latin-Square-of-Order k =
+  is-untruncated-π-finite-Main-Class-Latin-Hypercube-of-Order k 2
+
 is-π-finite-Main-Class-Latin-Square-of-Order :
-  (k m : ℕ) → is-π-finite k (Main-Class-Latin-Square-of-Order m)
-is-π-finite-Main-Class-Latin-Square-of-Order k m =
-  is-π-finite-Main-Class-Latin-Hypercube-of-Order k 2 m
+  (m : ℕ) → is-π-finite 1 (Main-Class-Latin-Square-of-Order m)
+is-π-finite-Main-Class-Latin-Square-of-Order =
+  is-π-finite-Main-Class-Latin-Hypercube-of-Order 2
 ```
 
 ### The sequence of the number of main classes of latin squares of finite order
diff --git a/src/univalent-combinatorics/pi-finite-types.lagda.md b/src/univalent-combinatorics/pi-finite-types.lagda.md
index 41814ae2aa..5632fede24 100644
--- a/src/univalent-combinatorics/pi-finite-types.lagda.md
+++ b/src/univalent-combinatorics/pi-finite-types.lagda.md
@@ -9,54 +9,17 @@ module univalent-combinatorics.pi-finite-types where
 ```agda
 open import elementary-number-theory.natural-numbers
 
-open import foundation.0-connected-types
-open import foundation.action-on-identifications-functions
-open import foundation.contractible-types
-open import foundation.coproduct-types
-open import foundation.decidable-propositions
-open import foundation.decidable-types
-open import foundation.dependent-identifications
-open import foundation.embeddings
-open import foundation.empty-types
-open import foundation.equality-coproduct-types
-open import foundation.equality-dependent-pair-types
-open import foundation.equivalences
-open import foundation.fiber-inclusions
-open import foundation.function-extensionality
-open import foundation.function-types
-open import foundation.functoriality-dependent-pair-types
-open import foundation.functoriality-set-truncation
-open import foundation.homotopies
+open import foundation.dependent-pair-types
 open import foundation.identity-types
-open import foundation.logical-equivalences
-open import foundation.maybe
-open import foundation.mere-equality
-open import foundation.propositional-extensionality
-open import foundation.propositional-truncations
 open import foundation.propositions
-open import foundation.retracts-of-types
-open import foundation.set-presented-types
 open import foundation.set-truncations
-open import foundation.sets
-open import foundation.subtypes
-open import foundation.surjective-maps
-open import foundation.transport-along-identifications
-open import foundation.type-arithmetic-coproduct-types
-open import foundation.unit-type
-open import foundation.univalence
+open import foundation.truncated-types
+open import foundation.truncation-levels
 open import foundation.universe-levels
-open import foundation.whiskering-homotopies-composition
 
-open import univalent-combinatorics.coproduct-types
-open import univalent-combinatorics.counting
-open import univalent-combinatorics.dependent-pair-types
-open import univalent-combinatorics.equality-finite-types
 open import univalent-combinatorics.finite-types
 open import univalent-combinatorics.finitely-many-connected-components
-open import univalent-combinatorics.finitely-presented-types
-open import univalent-combinatorics.function-types
-open import univalent-combinatorics.image-of-maps
-open import univalent-combinatorics.standard-finite-types
+open import univalent-combinatorics.untruncated-pi-finite-types
 ```
 
 </details>
@@ -64,599 +27,102 @@ open import univalent-combinatorics.standard-finite-types
 ## Idea
 
 A type is
-{{#concept "πₙ-finite" Disambiguation="type" Agda=is-π-finite Agda=π-Finite}} if
-it has [finitely](univalent-combinatorics.finite-types.md) many
-[connected components](foundation.connected-components.md) and all of its
-homotopy groups up to level `n` at all base points are finite.
+{{#concept "πₙ-finite" Disambiguation="type" Agda=is-π-finite Agda=π-Finite-Type}}
+if it has [finitely](univalent-combinatorics.finite-types.md) many
+[connected components](foundation.connected-components.md), all of its homotopy
+groups up to level `n` at all base points are finite, and all higher homotopy
+groups are [trivial](group-theory.trivial-groups.md). A type is
+{{#concept "π-finite"}} if it is πₙ-finite for some `n`.
 
 ## Definitions
 
-### π-finite types
+### The πₙ-finiteness predicate
 
 ```agda
 is-π-finite-Prop : {l : Level} (k : ℕ) → UU l → Prop l
-is-π-finite-Prop zero-ℕ X = has-finitely-many-connected-components-Prop X
+is-π-finite-Prop zero-ℕ X = is-finite-Prop X
 is-π-finite-Prop (succ-ℕ k) X =
   product-Prop
-    ( is-π-finite-Prop zero-ℕ X)
-    ( Π-Prop X (λ x → Π-Prop X (λ y → is-π-finite-Prop k (x ＝ y))))
+    ( has-finitely-many-connected-components-Prop X)
+    ( Π-Prop X
+      ( λ x → Π-Prop X (λ y → is-π-finite-Prop k (x ＝ y))))
 
 is-π-finite : {l : Level} (k : ℕ) → UU l → UU l
-is-π-finite k X = type-Prop (is-π-finite-Prop k X)
+is-π-finite k A =
+  type-Prop (is-π-finite-Prop k A)
 
 is-prop-is-π-finite :
-  {l : Level} (k : ℕ) (X : UU l) → is-prop (is-π-finite k X)
-is-prop-is-π-finite k X =
-  is-prop-type-Prop (is-π-finite-Prop k X)
-
-π-Finite : (l : Level) (k : ℕ) → UU (lsuc l)
-π-Finite l k = Σ (UU l) (is-π-finite k)
-
-type-π-Finite :
-  {l : Level} (k : ℕ) → π-Finite l k → UU l
-type-π-Finite k = pr1
-
-is-π-finite-type-π-Finite :
-  {l : Level} (k : ℕ) (A : π-Finite l k) →
-  is-π-finite k (type-π-Finite {l} k A)
-is-π-finite-type-π-Finite k = pr2
+  {l : Level} (k : ℕ) {A : UU l} → is-prop (is-π-finite k A)
+is-prop-is-π-finite k {A} =
+  is-prop-type-Prop (is-π-finite-Prop k A)
 
 has-finitely-many-connected-components-is-π-finite :
-  {l : Level} (k : ℕ) {A : UU l} →
-  is-π-finite k A → has-finitely-many-connected-components A
-has-finitely-many-connected-components-is-π-finite zero-ℕ H = H
-has-finitely-many-connected-components-is-π-finite (succ-ℕ k) H = pr1 H
-```
-
-## Properties
-
-### π-finite types are closed under equivalences
-
-```agda
-is-π-finite-equiv :
-  {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : UU l2} →
-  A ≃ B → is-π-finite k B → is-π-finite k A
-is-π-finite-equiv zero-ℕ =
-  has-finitely-many-connected-components-equiv'
-pr1 (is-π-finite-equiv (succ-ℕ k) e H) = is-π-finite-equiv zero-ℕ e (pr1 H)
-pr2 (is-π-finite-equiv (succ-ℕ k) e H) a b =
-  is-π-finite-equiv k
-    ( equiv-ap e a b)
-    ( pr2 H (map-equiv e a) (map-equiv e b))
-
-is-π-finite-equiv' :
-  {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : UU l2} →
-  A ≃ B → is-π-finite k A → is-π-finite k B
-is-π-finite-equiv' k e = is-π-finite-equiv k (inv-equiv e)
-```
-
-### π-finite types are closed under retracts
-
-```agda
-is-π-finite-retract :
-  {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : UU l2} →
-  A retract-of B → is-π-finite k B → is-π-finite k A
-is-π-finite-retract zero-ℕ = has-finitely-many-connected-components-retract
-pr1 (is-π-finite-retract (succ-ℕ k) r H) =
-  is-π-finite-retract zero-ℕ r
-    ( has-finitely-many-connected-components-is-π-finite (succ-ℕ k) H)
-pr2 (is-π-finite-retract (succ-ℕ k) r H) x y =
-  is-π-finite-retract k
-    ( retract-eq r x y)
-    ( pr2 H (inclusion-retract r x) (inclusion-retract r y))
-```
-
-### Empty types are π-finite
-
-```agda
-is-π-finite-empty : (k : ℕ) → is-π-finite k empty
-is-π-finite-empty zero-ℕ = has-finitely-many-connected-components-empty
-pr1 (is-π-finite-empty (succ-ℕ k)) = is-π-finite-empty zero-ℕ
-pr2 (is-π-finite-empty (succ-ℕ k)) = ind-empty
-
-empty-π-Finite : (k : ℕ) → π-Finite lzero k
-pr1 (empty-π-Finite k) = empty
-pr2 (empty-π-Finite k) = is-π-finite-empty k
-
-is-π-finite-is-empty :
-  {l : Level} (k : ℕ) {A : UU l} → is-empty A → is-π-finite k A
-is-π-finite-is-empty zero-ℕ = has-finitely-many-connected-components-is-empty
-pr1 (is-π-finite-is-empty (succ-ℕ k) f) = is-π-finite-is-empty zero-ℕ f
-pr2 (is-π-finite-is-empty (succ-ℕ k) f) a = ex-falso (f a)
-```
-
-### Contractible types are π-finite
-
-```agda
-is-π-finite-is-contr :
-  {l : Level} (k : ℕ) {A : UU l} → is-contr A → is-π-finite k A
-is-π-finite-is-contr zero-ℕ =
-  has-finitely-many-connected-components-is-contr
-pr1 (is-π-finite-is-contr (succ-ℕ k) H) = is-π-finite-is-contr zero-ℕ H
-pr2 (is-π-finite-is-contr (succ-ℕ k) H) x y =
-  is-π-finite-is-contr k ( is-prop-is-contr H x y)
-
-is-π-finite-unit : (k : ℕ) → is-π-finite k unit
-is-π-finite-unit k = is-π-finite-is-contr k is-contr-unit
-
-unit-π-Finite : (k : ℕ) → π-Finite lzero k
-pr1 (unit-π-Finite k) = unit
-pr2 (unit-π-Finite k) = is-π-finite-unit k
-```
-
-### Coproducts of π-finite types are π-finite
-
-```agda
-is-π-finite-coproduct :
-  {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : UU l2} →
-  is-π-finite k A → is-π-finite k B →
-  is-π-finite k (A + B)
-is-π-finite-coproduct zero-ℕ =
-  has-finitely-many-connected-components-coproduct
-pr1 (is-π-finite-coproduct (succ-ℕ k) H K) =
-  is-π-finite-coproduct zero-ℕ (pr1 H) (pr1 K)
-pr2 (is-π-finite-coproduct (succ-ℕ k) H K) (inl x) (inl y) =
-  is-π-finite-equiv k
-    ( compute-eq-coproduct-inl-inl x y)
-    ( pr2 H x y)
-pr2 (is-π-finite-coproduct (succ-ℕ k) H K) (inl x) (inr y) =
-  is-π-finite-equiv k
-    ( compute-eq-coproduct-inl-inr x y)
-    ( is-π-finite-empty k)
-pr2 (is-π-finite-coproduct (succ-ℕ k) H K) (inr x) (inl y) =
-  is-π-finite-equiv k
-    ( compute-eq-coproduct-inr-inl x y)
-    ( is-π-finite-empty k)
-pr2 (is-π-finite-coproduct (succ-ℕ k) H K) (inr x) (inr y) =
-  is-π-finite-equiv k
-    ( compute-eq-coproduct-inr-inr x y)
-    ( pr2 K x y)
-
-coproduct-π-Finite :
-  {l1 l2 : Level} (k : ℕ) →
-  π-Finite l1 k → π-Finite l2 k → π-Finite (l1 ⊔ l2) k
-pr1 (coproduct-π-Finite k A B) =
-  (type-π-Finite k A + type-π-Finite k B)
-pr2 (coproduct-π-Finite k A B) =
-  is-π-finite-coproduct k
-    ( is-π-finite-type-π-Finite k A)
-    ( is-π-finite-type-π-Finite k B)
+  {l : Level} (k : ℕ) {X : UU l} →
+  is-π-finite k X → has-finitely-many-connected-components X
+has-finitely-many-connected-components-is-π-finite zero-ℕ =
+  has-finitely-many-connected-components-is-finite
+has-finitely-many-connected-components-is-π-finite (succ-ℕ k) = pr1
 ```
 
-### `Maybe A` of any π-finite type `A` is π-finite
+### The subuniverse πₙ-finite types
 
 ```agda
-Maybe-π-Finite :
-  {l : Level} (k : ℕ) → π-Finite l k → π-Finite l k
-Maybe-π-Finite k A =
-  coproduct-π-Finite k A (unit-π-Finite k)
-
-is-π-finite-Maybe :
-  {l : Level} (k : ℕ) {A : UU l} →
-  is-π-finite k A → is-π-finite k (Maybe A)
-is-π-finite-Maybe k H =
-  is-π-finite-coproduct k H (is-π-finite-unit k)
-```
+π-Finite-Type : (l : Level) (k : ℕ) → UU (lsuc l)
+π-Finite-Type l k = Σ (UU l) (is-π-finite k)
 
-### Any stanadard finite type is π-finite
+type-π-Finite-Type :
+  {l : Level} (k : ℕ) → π-Finite-Type l k → UU l
+type-π-Finite-Type k = pr1
 
-```agda
-is-π-finite-Fin :
-  (k n : ℕ) → is-π-finite k (Fin n)
-is-π-finite-Fin k zero-ℕ =
-  is-π-finite-empty k
-is-π-finite-Fin k (succ-ℕ n) =
-  is-π-finite-Maybe k (is-π-finite-Fin k n)
-
-Fin-π-Finite : (k : ℕ) (n : ℕ) → π-Finite lzero k
-pr1 (Fin-π-Finite k n) = Fin n
-pr2 (Fin-π-Finite k n) = is-π-finite-Fin k n
+is-π-finite-type-π-Finite-Type :
+  {l : Level} (k : ℕ) (A : π-Finite-Type l k) →
+  is-π-finite k (type-π-Finite-Type {l} k A)
+is-π-finite-type-π-Finite-Type k = pr2
 ```
 
-### Any type equipped with a counting is π-finite
-
-```agda
-is-π-finite-count :
-  {l : Level} (k : ℕ) {A : UU l} → count A → is-π-finite k A
-is-π-finite-count k (n , e) =
-  is-π-finite-equiv' k e (is-π-finite-Fin k n)
-```
-
-### Any finite type is π-finite
-
-```agda
-is-π-finite-is-finite :
-  {l : Level} (k : ℕ) {A : UU l} → is-finite A → is-π-finite k A
-is-π-finite-is-finite k {A} H =
-  apply-universal-property-trunc-Prop H
-    ( is-π-finite-Prop k A)
-    ( is-π-finite-count k)
-
-π-finite-𝔽 : {l : Level} (k : ℕ) → 𝔽 l → π-Finite l k
-pr1 (π-finite-𝔽 k A) = type-𝔽 A
-pr2 (π-finite-𝔽 k A) = is-π-finite-is-finite k (is-finite-type-𝔽 A)
-```
+## Properties
 
-### The type of all `n`-element types in `UU l` is π-finite
+### πₙ-finite types are n-truncated
 
 ```agda
-is-π-finite-UU-Fin :
-  {l : Level} (k n : ℕ) → is-π-finite k (UU-Fin l n)
-is-π-finite-UU-Fin zero-ℕ n =
-  has-finitely-many-connected-components-UU-Fin n
-pr1 (is-π-finite-UU-Fin (succ-ℕ k) n) =
-  is-π-finite-UU-Fin zero-ℕ n
-pr2 (is-π-finite-UU-Fin (succ-ℕ k) n) x y =
-  is-π-finite-equiv k
-    ( equiv-equiv-eq-UU-Fin n x y)
-    ( is-π-finite-is-finite k
-      ( is-finite-≃
-        ( is-finite-has-finite-cardinality (n , pr2 x))
-        ( is-finite-has-finite-cardinality (n , pr2 y))))
+is-trunc-is-π-finite :
+  {l : Level} (k : ℕ) {X : UU l} →
+  is-π-finite k X → is-trunc (truncation-level-ℕ k) X
+is-trunc-is-π-finite zero-ℕ = is-set-is-finite
+is-trunc-is-π-finite (succ-ℕ k) H x y =
+  is-trunc-is-π-finite k (pr2 H x y)
 ```
 
-### πₙ₊₁-finite types are πₙ-finite
+### Untruncated πₙ-finite n-truncated types are πₙ-finite
 
 ```agda
-is-π-finite-is-π-finite-succ-ℕ :
-  {l : Level} (k : ℕ) {A : UU l} →
-  is-π-finite (succ-ℕ k) A → is-π-finite k A
-is-π-finite-is-π-finite-succ-ℕ zero-ℕ H =
-  has-finitely-many-connected-components-is-π-finite 1 H
-pr1 (is-π-finite-is-π-finite-succ-ℕ (succ-ℕ k) H) =
-  has-finitely-many-connected-components-is-π-finite (succ-ℕ (succ-ℕ k)) H
-pr2 (is-π-finite-is-π-finite-succ-ℕ (succ-ℕ k) H) x y =
-  is-π-finite-is-π-finite-succ-ℕ k (pr2 H x y)
+is-π-finite-is-untruncated-π-finite :
+  {l : Level} (k : ℕ) {A : UU l} → is-trunc (truncation-level-ℕ k) A →
+  is-untruncated-π-finite k A → is-π-finite k A
+is-π-finite-is-untruncated-π-finite zero-ℕ H K =
+  is-finite-is-untruncated-π-finite zero-ℕ H K
+pr1 (is-π-finite-is-untruncated-π-finite (succ-ℕ k) H K) = pr1 K
+pr2 (is-π-finite-is-untruncated-π-finite (succ-ℕ k) H K) x y =
+  is-π-finite-is-untruncated-π-finite k (H x y) (pr2 K x y)
 ```
 
-### πₙ₊₁-finite types are π₁-finite
+### πₙ-finite types are untruncated πₙ-finite
 
 ```agda
-is-π-finite-one-is-π-finite-succ-ℕ :
+is-untruncated-π-finite-is-π-finite :
   {l : Level} (k : ℕ) {A : UU l} →
-  is-π-finite (succ-ℕ k) A → is-π-finite 1 A
-is-π-finite-one-is-π-finite-succ-ℕ zero-ℕ H = H
-is-π-finite-one-is-π-finite-succ-ℕ (succ-ℕ k) H =
-  is-π-finite-one-is-π-finite-succ-ℕ k
-    ( is-π-finite-is-π-finite-succ-ℕ (succ-ℕ k) H)
-```
-
-### πₙ-finite sets are finite
-
-```agda
-is-finite-is-π-finite :
-  {l : Level} (k : ℕ) {A : UU l} → is-set A →
-  is-π-finite k A → is-finite A
-is-finite-is-π-finite k H K =
-  is-finite-equiv'
-    ( equiv-unit-trunc-Set (_ , H))
-    ( has-finitely-many-connected-components-is-π-finite k K)
-```
-
-### Finite products of π-finite types are π-finite
-
-```agda
-is-π-finite-Π :
-  {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : A → UU l2} →
-  is-finite A → ((a : A) → is-π-finite k (B a)) →
-  is-π-finite k ((a : A) → B a)
-is-π-finite-Π zero-ℕ =
-  has-finitely-many-connected-components-finite-Π
-pr1 (is-π-finite-Π (succ-ℕ k) H K) =
-  is-π-finite-Π zero-ℕ H (λ a → pr1 (K a))
-pr2 (is-π-finite-Π (succ-ℕ k) H K) f g =
-  is-π-finite-equiv k
-    ( equiv-funext)
-    ( is-π-finite-Π k H (λ a → pr2 (K a) (f a) (g a)))
-
-π-Finite-Π :
-  {l1 l2 : Level} (k : ℕ) (A : 𝔽 l1) (B : type-𝔽 A → π-Finite l2 k) →
-  π-Finite (l1 ⊔ l2) k
-pr1 (π-Finite-Π k A B) =
-  (x : type-𝔽 A) → (type-π-Finite k (B x))
-pr2 (π-Finite-Π k A B) =
-  is-π-finite-Π k
-    ( is-finite-type-𝔽 A)
-    ( λ x → is-π-finite-type-π-Finite k (B x))
-```
-
-### Dependent sums of types with finitely many connected components over a `0`-connected base
-
-The total space of a family of types with finitely many connected components
-over a `0`-connected base has finitely many connected components when the based
-[loop spaces](synthetic-homotopy-theory.loop-spaces.md) of the base have
-finitely many connected components.
-
-```agda
-has-finitely-many-connected-components-Σ-is-0-connected :
-  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
-  is-0-connected A →
-  ((a : A) → has-finitely-many-connected-components (a ＝ a)) →
-  ((x : A) → has-finitely-many-connected-components (B x)) →
-  has-finitely-many-connected-components (Σ A B)
-has-finitely-many-connected-components-Σ-is-0-connected {A = A} {B} C H K =
-  apply-universal-property-trunc-Prop
-    ( is-inhabited-is-0-connected C)
-    ( has-finitely-many-connected-components-Prop (Σ A B))
-    ( α)
-  where
-  α : A → has-finitely-many-connected-components (Σ A B)
-  α a =
-    is-finite-codomain
-      ( K a)
-      ( is-surjective-map-trunc-Set
-        ( fiber-inclusion B a)
-        ( is-surjective-fiber-inclusion C a))
-      ( apply-dependent-universal-property-trunc-Set'
-        ( λ x →
-          set-Prop
-            ( Π-Prop
-              ( type-trunc-Set (Σ A B))
-              ( λ y → is-decidable-Prop (Id-Prop (trunc-Set (Σ A B)) x y))))
-        ( β))
-    where
-    β :
-      (x : Σ A B) (v : type-trunc-Set (Σ A B)) →
-      is-decidable (unit-trunc-Set x ＝ v)
-    β (x , y) =
-      apply-dependent-universal-property-trunc-Set'
-        ( λ u →
-          set-Prop
-            ( is-decidable-Prop
-              ( Id-Prop (trunc-Set (Σ A B)) (unit-trunc-Set (x , y)) u)))
-        ( γ)
-      where
-      γ :
-        (v : Σ A B) →
-        is-decidable ((unit-trunc-Set (x , y)) ＝ (unit-trunc-Set v))
-      γ (x' , y') =
-        is-decidable-equiv
-          ( is-effective-unit-trunc-Set
-            ( Σ A B)
-            ( x , y)
-            ( x' , y'))
-          ( apply-universal-property-trunc-Prop
-            ( mere-eq-is-0-connected C a x)
-            ( is-decidable-Prop
-              ( mere-eq-Prop (x , y) (x' , y')))
-              ( δ))
-        where
-        δ : a ＝ x → is-decidable (mere-eq (x , y) (x' , y'))
-        δ refl =
-          apply-universal-property-trunc-Prop
-            ( mere-eq-is-0-connected C a x')
-            ( is-decidable-Prop
-              ( mere-eq-Prop (a , y) (x' , y')))
-            ( ε)
-          where
-          ε : a ＝ x' → is-decidable (mere-eq (x , y) (x' , y'))
-          ε refl =
-            is-decidable-equiv e
-              ( is-decidable-type-trunc-Prop-is-finite
-                ( is-finite-Σ
-                  ( H a)
-                  ( λ ω → is-finite-is-decidable-Prop (P ω) (d ω))))
-            where
-            ℙ :
-              is-contr
-                ( Σ ( hom-Set (trunc-Set (a ＝ a)) (Prop-Set _))
-                    ( λ h →
-                      ( λ a₁ → h (unit-trunc-Set a₁)) ~
-                      ( λ ω₁ →
-                        trunc-Prop (dependent-identification B ω₁ y y'))))
-            ℙ =
-              universal-property-trunc-Set
-                ( a ＝ a)
-                ( Prop-Set _)
-                ( λ ω → trunc-Prop (dependent-identification B ω y y'))
-
-            P : type-trunc-Set (Id a a) → Prop _
-            P = pr1 (center ℙ)
-
-            compute-P :
-              (ω : a ＝ a) →
-              type-Prop (P (unit-trunc-Set ω)) ≃
-              type-trunc-Prop (dependent-identification B ω y y')
-            compute-P ω = equiv-eq (ap pr1 (pr2 (center ℙ) ω))
-
-            d : (t : type-trunc-Set (a ＝ a)) → is-decidable (type-Prop (P t))
-            d =
-              apply-dependent-universal-property-trunc-Set'
-                ( λ t → set-Prop (is-decidable-Prop (P t)))
-                ( λ ω →
-                  is-decidable-equiv'
-                    ( inv-equiv (compute-P ω))
-                    ( is-decidable-equiv'
-                      ( is-effective-unit-trunc-Set (B a) (tr B ω y) y')
-                      ( has-decidable-equality-is-finite
-                        ( K a)
-                        ( unit-trunc-Set (tr B ω y))
-                        ( unit-trunc-Set y'))))
-
-            f : type-hom-Prop
-                ( trunc-Prop (Σ (type-trunc-Set (Id a a)) (type-Prop ∘ P)))
-                ( mere-eq-Prop {A = Σ A B} (a , y) (a , y'))
-            f t =
-              apply-universal-property-trunc-Prop t
-                ( mere-eq-Prop (a , y) (a , y'))
-                  λ (u , v) →
-                  apply-dependent-universal-property-trunc-Set'
-                    ( λ u' →
-                      hom-set-Set
-                        ( set-Prop (P u'))
-                        ( set-Prop
-                          ( mere-eq-Prop (a , y) (a , y'))))
-                    ( λ ω v' →
-                      apply-universal-property-trunc-Prop
-                        ( map-equiv (compute-P ω) v')
-                        ( mere-eq-Prop (a , y) (a , y'))
-                        ( λ p → unit-trunc-Prop (eq-pair-Σ ω p)))
-                    ( u)
-                    ( v)
-            e :
-              mere-eq {A = Σ A B} (a , y) (a , y') ≃
-              type-trunc-Prop (Σ (type-trunc-Set (Id a a)) (type-Prop ∘ P))
-            e =
-              equiv-iff
-                ( mere-eq-Prop (a , y) (a , y'))
-                ( trunc-Prop (Σ (type-trunc-Set (a ＝ a)) (type-Prop ∘ P)))
-                ( λ t →
-                  apply-universal-property-trunc-Prop t
-                    ( trunc-Prop _)
-                    ( ( λ (ω , r) →
-                        unit-trunc-Prop
-                          { A = Σ (type-trunc-Set (a ＝ a)) (type-Prop ∘ P)}
-                          ( ( unit-trunc-Set ω) ,
-                            ( map-inv-equiv
-                              ( compute-P ω)
-                              ( unit-trunc-Prop r)))) ∘
-                      ( pair-eq-Σ)))
-                ( f)
-```
-
-### Dependent sums of types with finitely many connected components
-
-```agda
-abstract
-  has-finitely-many-connected-components-Σ' :
-    {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : A → UU l2} →
-    (Fin k ≃ type-trunc-Set A) →
-    ((x y : A) → has-finitely-many-connected-components (x ＝ y)) →
-    ((x : A) → has-finitely-many-connected-components (B x)) →
-    has-finitely-many-connected-components (Σ A B)
-  has-finitely-many-connected-components-Σ' zero-ℕ e H K =
-    has-finitely-many-connected-components-is-empty
-      ( is-empty-is-empty-trunc-Set (map-inv-equiv e) ∘ pr1)
-  has-finitely-many-connected-components-Σ' (succ-ℕ k) {A} {B} e H K =
-    apply-universal-property-trunc-Prop
-      ( has-presentation-of-cardinality-has-cardinality-connected-components
-        ( succ-ℕ k)
-        ( unit-trunc-Prop e))
-      ( has-finitely-many-connected-components-Prop (Σ A B))
-      ( α)
-    where
-    α : Σ (Fin (succ-ℕ k) → A) (λ f → is-equiv (unit-trunc-Set ∘ f)) →
-        has-finitely-many-connected-components (Σ A B)
-    α (f , Eηf) =
-      is-finite-equiv
-        ( equiv-trunc-Set g)
-        ( is-finite-equiv'
-          ( equiv-distributive-trunc-coproduct-Set
-            ( Σ (im (f ∘ inl)) (B ∘ pr1))
-            ( Σ (im (f ∘ inr)) (B ∘ pr1)))
-          ( is-finite-coproduct
-            ( has-finitely-many-connected-components-Σ' k
-              ( h)
-              ( λ x y →
-                is-finite-equiv'
-                  ( equiv-trunc-Set
-                    ( equiv-ap-emb
-                      ( pr1 , is-emb-inclusion-subtype ( λ u → trunc-Prop _))))
-                  ( H (pr1 x) (pr1 y)))
-              ( λ x → K (pr1 x)))
-            ( has-finitely-many-connected-components-Σ-is-0-connected
-              ( is-0-connected-im-is-0-connected-domain
-                ( f ∘ inr)
-                ( is-0-connected-unit))
-              ( λ a →
-                has-finitely-many-connected-components-equiv'
-                  ( equiv-Eq-eq-im (f ∘ inr) a a)
-                  ( H (pr1 a) (pr1 a)))
-              ( λ x → K (pr1 x)))))
-      where
-      g : ((Σ (im (f ∘ inl)) (B ∘ pr1)) + (Σ (im (f ∘ inr)) (B ∘ pr1))) ≃
-          Σ A B
-      g =
-        ( equiv-Σ B
-          ( is-coproduct-codomain f
-            ( unit-trunc-Set ∘ f , Eηf)
-            ( refl-htpy))
-          ( λ { (inl x) → id-equiv ; (inr x) → id-equiv})) ∘e
-        ( inv-equiv
-          ( right-distributive-Σ-coproduct
-            ( im (f ∘ inl))
-            ( im (f ∘ inr))
-            ( rec-coproduct (B ∘ pr1) (B ∘ pr1))))
-
-      i : Fin k → type-trunc-Set (im (f ∘ inl))
-      i = unit-trunc-Set ∘ map-unit-im (f ∘ inl)
-
-      is-surjective-i : is-surjective i
-      is-surjective-i =
-        is-surjective-comp
-          ( is-surjective-unit-trunc-Set (im (f ∘ inl)))
-          ( is-surjective-map-unit-im (f ∘ inl))
-
-      is-emb-i : is-emb i
-      is-emb-i =
-        is-emb-top-map-triangle
-          ( (unit-trunc-Set ∘ f) ∘ inl)
-          ( inclusion-trunc-im-Set (f ∘ inl))
-          ( i)
-          ( ( inv-htpy (naturality-unit-trunc-Set (inclusion-im (f ∘ inl)))) ·r
-            ( map-unit-im (f ∘ inl)))
-          ( is-emb-inclusion-trunc-im-Set (f ∘ inl))
-          ( is-emb-comp
-            ( unit-trunc-Set ∘ f)
-            ( inl)
-            ( is-emb-is-equiv Eηf)
-            ( is-emb-inl))
-      h : Fin k ≃ type-trunc-Set (im (f ∘ inl))
-      h = i , (is-equiv-is-emb-is-surjective is-surjective-i is-emb-i)
-```
-
-### Dependent sums of π-finite types
-
-The dependent sum of a family of πₙ-finite types over a πₙ₊₁-finite base is
-πₙ-finite.
-
-```agda
-has-finitely-many-connected-components-Σ :
-  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
-  is-π-finite 1 A →
-  ((x : A) → has-finitely-many-connected-components (B x)) →
-  has-finitely-many-connected-components (Σ A B)
-has-finitely-many-connected-components-Σ {A = A} {B} H K =
-  apply-universal-property-trunc-Prop
-    ( pr1 H)
-    ( has-finitely-many-connected-components-Prop (Σ A B))
-    ( λ (k , e) →
-      has-finitely-many-connected-components-Σ' k e (λ x y → pr2 H x y) K)
-
-abstract
-  is-π-finite-Σ :
-    {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : A → UU l2} →
-    is-π-finite (succ-ℕ k) A → ((x : A) → is-π-finite k (B x)) →
-    is-π-finite k (Σ A B)
-  is-π-finite-Σ zero-ℕ =
-    has-finitely-many-connected-components-Σ
-  pr1 (is-π-finite-Σ (succ-ℕ k) H K) =
-    has-finitely-many-connected-components-Σ
-      ( is-π-finite-one-is-π-finite-succ-ℕ (succ-ℕ k) H)
-      ( λ x →
-        has-finitely-many-connected-components-is-π-finite (succ-ℕ k) (K x))
-  pr2 (is-π-finite-Σ (succ-ℕ k) H K) (x , u) (y , v) =
-    is-π-finite-equiv k
-      ( equiv-pair-eq-Σ (x , u) (y , v))
-      ( is-π-finite-Σ k
-        ( pr2 H x y)
-        ( λ where refl → pr2 (K x) u v))
-
-π-Finite-Σ :
-  {l1 l2 : Level} (k : ℕ) (A : π-Finite l1 (succ-ℕ k))
-  (B : (x : type-π-Finite (succ-ℕ k) A) → π-Finite l2 k) →
-  π-Finite (l1 ⊔ l2) k
-pr1 (π-Finite-Σ k A B) =
-  Σ (type-π-Finite (succ-ℕ k) A) (λ x → type-π-Finite k (B x))
-pr2 (π-Finite-Σ k A B) =
-  is-π-finite-Σ k
-    ( is-π-finite-type-π-Finite (succ-ℕ k) A)
-    ( λ x → is-π-finite-type-π-Finite k (B x))
+  is-π-finite k A → is-untruncated-π-finite k A
+is-untruncated-π-finite-is-π-finite zero-ℕ H =
+  is-finite-equiv
+    ( equiv-unit-trunc-Set (_ , (is-set-is-finite H)))
+    ( H)
+pr1 (is-untruncated-π-finite-is-π-finite (succ-ℕ k) H) = pr1 H
+pr2 (is-untruncated-π-finite-is-π-finite (succ-ℕ k) H) x y =
+  is-untruncated-π-finite-is-π-finite k (pr2 H x y)
 ```
 
 ## See also
 
-- [Truncated π-finite types](univalent-combinatorics.truncated-pi-finite-types.md)
 - [Unbounded π-finite types](univalent-combinatorics.unbounded-pi-finite-types.md)
 
 ## External links
diff --git a/src/univalent-combinatorics/truncated-pi-finite-types.lagda.md b/src/univalent-combinatorics/truncated-pi-finite-types.lagda.md
deleted file mode 100644
index aef946deb7..0000000000
--- a/src/univalent-combinatorics/truncated-pi-finite-types.lagda.md
+++ /dev/null
@@ -1,109 +0,0 @@
-# Truncated π-finite types
-
-```agda
-module univalent-combinatorics.truncated-pi-finite-types where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import elementary-number-theory.natural-numbers
-
-open import foundation.dependent-pair-types
-open import foundation.identity-types
-open import foundation.propositions
-open import foundation.set-truncations
-open import foundation.truncated-types
-open import foundation.truncation-levels
-open import foundation.universe-levels
-
-open import univalent-combinatorics.finite-types
-open import univalent-combinatorics.finitely-many-connected-components
-open import univalent-combinatorics.pi-finite-types
-```
-
-</details>
-
-## Idea
-
-A type is
-{{#concept "truncated πₙ-finite" Disambiguation="type" Agda=is-truncated-π-finite Agda=Truncated-π-Finite}}
-if it has [finitely](univalent-combinatorics.finite-types.md) many
-[connected components](foundation.connected-components.md), all of its homotopy
-groups up to level `n` at all base points are finite, and all higher homotopy
-groups are [trivial](group-theory.trivial-groups.md).
-
-## Definitions
-
-### Truncated π-finite types
-
-```agda
-is-truncated-π-finite-Prop : {l : Level} (k : ℕ) → UU l → Prop l
-is-truncated-π-finite-Prop zero-ℕ X = is-finite-Prop X
-is-truncated-π-finite-Prop (succ-ℕ k) X =
-  product-Prop
-    ( has-finitely-many-connected-components-Prop X)
-    ( Π-Prop X
-      ( λ x → Π-Prop X (λ y → is-truncated-π-finite-Prop k (x ＝ y))))
-
-is-truncated-π-finite : {l : Level} (k : ℕ) → UU l → UU l
-is-truncated-π-finite k A =
-  type-Prop (is-truncated-π-finite-Prop k A)
-
-is-prop-is-truncated-π-finite :
-  {l : Level} (k : ℕ) {A : UU l} → is-prop (is-truncated-π-finite k A)
-is-prop-is-truncated-π-finite k {A} =
-  is-prop-type-Prop (is-truncated-π-finite-Prop k A)
-
-has-finitely-many-connected-components-is-truncated-π-finite :
-  {l : Level} (k : ℕ) {X : UU l} →
-  is-truncated-π-finite k X → has-finitely-many-connected-components X
-has-finitely-many-connected-components-is-truncated-π-finite zero-ℕ =
-  has-finitely-many-connected-components-is-finite
-has-finitely-many-connected-components-is-truncated-π-finite (succ-ℕ k) = pr1
-```
-
-## Properties
-
-### Truncated πₙ-finite types are n-truncated
-
-```agda
-is-trunc-is-truncated-π-finite :
-  {l : Level} (k : ℕ) {X : UU l} →
-  is-truncated-π-finite k X → is-trunc (truncation-level-ℕ k) X
-is-trunc-is-truncated-π-finite zero-ℕ = is-set-is-finite
-is-trunc-is-truncated-π-finite (succ-ℕ k) H x y =
-  is-trunc-is-truncated-π-finite k (pr2 H x y)
-```
-
-### πₙ-finite n-truncated types are truncated πₙ-finite
-
-```agda
-is-truncated-π-finite-is-π-finite :
-  {l : Level} (k : ℕ) {A : UU l} → is-trunc (truncation-level-ℕ k) A →
-  is-π-finite k A → is-truncated-π-finite k A
-is-truncated-π-finite-is-π-finite zero-ℕ H K =
-  is-finite-is-π-finite zero-ℕ H K
-pr1 (is-truncated-π-finite-is-π-finite (succ-ℕ k) H K) = pr1 K
-pr2 (is-truncated-π-finite-is-π-finite (succ-ℕ k) H K) x y =
-  is-truncated-π-finite-is-π-finite k (H x y) (pr2 K x y)
-```
-
-### Truncated πₙ-finite types are πₙ-finite
-
-```agda
-is-π-finite-is-truncated-π-finite :
-  {l : Level} (k : ℕ) {A : UU l} →
-  is-truncated-π-finite k A → is-π-finite k A
-is-π-finite-is-truncated-π-finite zero-ℕ H =
-  is-finite-equiv
-    ( equiv-unit-trunc-Set (_ , (is-set-is-finite H)))
-    ( H)
-pr1 (is-π-finite-is-truncated-π-finite (succ-ℕ k) H) = pr1 H
-pr2 (is-π-finite-is-truncated-π-finite (succ-ℕ k) H) x y =
-  is-π-finite-is-truncated-π-finite k (pr2 H x y)
-```
-
-## See also
-
-- [Unbounded π-finite types](univalent-combinatorics.unbounded-pi-finite-types.md)
diff --git a/src/univalent-combinatorics/unbounded-pi-finite-types.lagda.md b/src/univalent-combinatorics/unbounded-pi-finite-types.lagda.md
index 56e7c6c026..91a63364e5 100644
--- a/src/univalent-combinatorics/unbounded-pi-finite-types.lagda.md
+++ b/src/univalent-combinatorics/unbounded-pi-finite-types.lagda.md
@@ -34,7 +34,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.truncated-pi-finite-types
+open import univalent-combinatorics.untruncated-pi-finite-types
 ```
 
 </details>
@@ -341,49 +341,53 @@ is-finite-is-unbounded-π-finite H K =
     ( has-finitely-many-connected-components-is-unbounded-π-finite K)
 ```
 
-### Truncated π-finite types are unbounded π-finite
+### π-finite types are unbounded π-finite
 
 ```agda
-is-unbounded-π-finite-is-truncated-π-finite :
+is-unbounded-π-finite-is-π-finite :
   {l : Level} (k : ℕ) {A : UU l} →
-  is-truncated-π-finite k A → is-unbounded-π-finite A
-is-unbounded-π-finite-is-truncated-π-finite zero-ℕ =
+  is-π-finite k A → is-unbounded-π-finite A
+is-unbounded-π-finite-is-π-finite zero-ℕ =
   is-unbounded-π-finite-is-finite
-is-unbounded-π-finite-is-truncated-π-finite (succ-ℕ k) H =
+is-unbounded-π-finite-is-π-finite (succ-ℕ k) H =
   λ where
   .has-finitely-many-connected-components-is-unbounded-π-finite →
     pr1 H
   .is-unbounded-π-finite-Id-is-unbounded-π-finite x y →
-    is-unbounded-π-finite-is-truncated-π-finite k (pr2 H x y)
+    is-unbounded-π-finite-is-π-finite k (pr2 H x y)
 ```
 
-### Unbounded π-finite types are types that are πₙ-finite for all `n`
+### Unbounded π-finite types are types that are untruncated πₙ-finite for all `n`
 
 ```agda
 is-unbounded-π-finite-Id-is-unbounded-π-finite' :
   {l : Level} {A : UU l} →
-  ((k : ℕ) → is-π-finite k A) →
+  ((k : ℕ) → is-untruncated-π-finite k A) →
   (x y : A) →
-  (k : ℕ) → is-π-finite k (x ＝ y)
+  (k : ℕ) → is-untruncated-π-finite k (x ＝ y)
 is-unbounded-π-finite-Id-is-unbounded-π-finite' H x y k = pr2 (H (succ-ℕ k)) x y
 
-is-unbounded-π-finite-is-π-finite :
-  {l : Level} {A : UU l} → ((k : ℕ) → is-π-finite k A) → is-unbounded-π-finite A
-is-unbounded-π-finite-is-π-finite H =
+is-unbounded-π-finite-is-untruncated-π-finite :
+  {l : Level} {A : UU l} →
+  ((k : ℕ) → is-untruncated-π-finite k A) →
+  is-unbounded-π-finite A
+is-unbounded-π-finite-is-untruncated-π-finite H =
   λ where
   .has-finitely-many-connected-components-is-unbounded-π-finite → H 0
   .is-unbounded-π-finite-Id-is-unbounded-π-finite x y →
-    is-unbounded-π-finite-is-π-finite
+    is-unbounded-π-finite-is-untruncated-π-finite
       ( is-unbounded-π-finite-Id-is-unbounded-π-finite' H x y)
 
-is-π-finite-is-unbounded-π-finite :
-  {l : Level} {A : UU l} → is-unbounded-π-finite A → (k : ℕ) → is-π-finite k A
-is-π-finite-is-unbounded-π-finite H zero-ℕ =
+is-untruncated-π-finite-is-unbounded-π-finite :
+  {l : Level} {A : UU l} →
+  is-unbounded-π-finite A →
+  (k : ℕ) → is-untruncated-π-finite k A
+is-untruncated-π-finite-is-unbounded-π-finite H zero-ℕ =
   has-finitely-many-connected-components-is-unbounded-π-finite H
-pr1 (is-π-finite-is-unbounded-π-finite H (succ-ℕ k)) =
-  is-π-finite-is-unbounded-π-finite H zero-ℕ
-pr2 (is-π-finite-is-unbounded-π-finite H (succ-ℕ k)) x y =
-  is-π-finite-is-unbounded-π-finite
+pr1 (is-untruncated-π-finite-is-unbounded-π-finite H (succ-ℕ k)) =
+  is-untruncated-π-finite-is-unbounded-π-finite H zero-ℕ
+pr2 (is-untruncated-π-finite-is-unbounded-π-finite H (succ-ℕ k)) x y =
+  is-untruncated-π-finite-is-unbounded-π-finite
     ( is-unbounded-π-finite-Id-is-unbounded-π-finite H x y)
     ( k)
 ```
@@ -412,7 +416,7 @@ is-unbounded-π-finite-Π H K =
 ```
 
 Instead, we give a proof using the description of unbounded π-finite types as
-types that are πₙ-finite for all n.
+types that are untruncated πₙ-finite for all n.
 
 ```agda
 is-unbounded-π-finite-Π :
@@ -420,10 +424,10 @@ is-unbounded-π-finite-Π :
   is-finite A → ((a : A) → is-unbounded-π-finite (B a)) →
   is-unbounded-π-finite ((a : A) → B a)
 is-unbounded-π-finite-Π H K =
-  is-unbounded-π-finite-is-π-finite
+  is-unbounded-π-finite-is-untruncated-π-finite
     ( λ k →
-      is-π-finite-Π k H
-        ( λ a → is-π-finite-is-unbounded-π-finite (K a) k))
+      is-untruncated-π-finite-Π k H
+        ( λ a → is-untruncated-π-finite-is-unbounded-π-finite (K a) k))
 ```
 
 ### Dependent sums of unbounded π-finite types are unbounded π-finite
@@ -438,11 +442,11 @@ abstract
     is-unbounded-π-finite A → ((x : A) → is-unbounded-π-finite (B x)) →
     is-unbounded-π-finite (Σ A B)
   is-unbounded-π-finite-Σ H K =
-    is-unbounded-π-finite-is-π-finite
+    is-unbounded-π-finite-is-untruncated-π-finite
       ( λ k →
-        is-π-finite-Σ k
-          ( is-π-finite-is-unbounded-π-finite H (succ-ℕ k))
-          ( λ x → is-π-finite-is-unbounded-π-finite (K x) k))
+        is-untruncated-π-finite-Σ k
+          ( is-untruncated-π-finite-is-unbounded-π-finite H (succ-ℕ k))
+          ( λ x → is-untruncated-π-finite-is-unbounded-π-finite (K x) k))
 ```
 
 ## References
diff --git a/src/univalent-combinatorics/untruncated-pi-finite-types.lagda.md b/src/univalent-combinatorics/untruncated-pi-finite-types.lagda.md
new file mode 100644
index 0000000000..2a527431b1
--- /dev/null
+++ b/src/univalent-combinatorics/untruncated-pi-finite-types.lagda.md
@@ -0,0 +1,691 @@
+# Untruncated π-finite types
+
+```agda
+module univalent-combinatorics.untruncated-pi-finite-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.0-connected-types
+open import foundation.action-on-identifications-functions
+open import foundation.contractible-types
+open import foundation.coproduct-types
+open import foundation.decidable-propositions
+open import foundation.decidable-types
+open import foundation.dependent-identifications
+open import foundation.embeddings
+open import foundation.empty-types
+open import foundation.equality-coproduct-types
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.fiber-inclusions
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.functoriality-set-truncation
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.maybe
+open import foundation.mere-equality
+open import foundation.propositional-extensionality
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.retracts-of-types
+open import foundation.set-presented-types
+open import foundation.set-truncations
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.surjective-maps
+open import foundation.transport-along-identifications
+open import foundation.type-arithmetic-coproduct-types
+open import foundation.unit-type
+open import foundation.univalence
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import univalent-combinatorics.coproduct-types
+open import univalent-combinatorics.counting
+open import univalent-combinatorics.dependent-pair-types
+open import univalent-combinatorics.equality-finite-types
+open import univalent-combinatorics.finite-types
+open import univalent-combinatorics.finitely-many-connected-components
+open import univalent-combinatorics.finitely-presented-types
+open import univalent-combinatorics.function-types
+open import univalent-combinatorics.image-of-maps
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+A type is
+{{#concept "untruncated πₙ-finite" Disambiguation="type" Agda=is-untruncated-π-finite Agda=Untruncated-π-Finite-Type}}
+if it has [finitely](univalent-combinatorics.finite-types.md) many
+[connected components](foundation.connected-components.md) and all of its
+homotopy groups up to level `n` at all base points are finite.
+
+## Definitions
+
+### The untruncated πₙ-finiteness predicate
+
+```agda
+is-untruncated-π-finite-Prop : {l : Level} (k : ℕ) → UU l → Prop l
+is-untruncated-π-finite-Prop zero-ℕ X =
+  has-finitely-many-connected-components-Prop X
+is-untruncated-π-finite-Prop (succ-ℕ k) X =
+  product-Prop
+    ( is-untruncated-π-finite-Prop zero-ℕ X)
+    ( Π-Prop X (λ x → Π-Prop X (λ y → is-untruncated-π-finite-Prop k (x ＝ y))))
+
+is-untruncated-π-finite : {l : Level} (k : ℕ) → UU l → UU l
+is-untruncated-π-finite k X = type-Prop (is-untruncated-π-finite-Prop k X)
+
+is-prop-is-untruncated-π-finite :
+  {l : Level} (k : ℕ) (X : UU l) → is-prop (is-untruncated-π-finite k X)
+is-prop-is-untruncated-π-finite k X =
+  is-prop-type-Prop (is-untruncated-π-finite-Prop k X)
+
+has-finitely-many-connected-components-is-untruncated-π-finite :
+  {l : Level} (k : ℕ) {A : UU l} →
+  is-untruncated-π-finite k A → has-finitely-many-connected-components A
+has-finitely-many-connected-components-is-untruncated-π-finite zero-ℕ H = H
+has-finitely-many-connected-components-is-untruncated-π-finite (succ-ℕ k) H =
+  pr1 H
+```
+
+### The subuniverse untruncated πₙ-finite types
+
+```agda
+Untruncated-π-Finite-Type : (l : Level) (k : ℕ) → UU (lsuc l)
+Untruncated-π-Finite-Type l k = Σ (UU l) (is-untruncated-π-finite k)
+
+type-Untruncated-π-Finite-Type :
+  {l : Level} (k : ℕ) → Untruncated-π-Finite-Type l k → UU l
+type-Untruncated-π-Finite-Type k = pr1
+
+is-untruncated-π-finite-type-Untruncated-π-Finite-Type :
+  {l : Level} (k : ℕ) (A : Untruncated-π-Finite-Type l k) →
+  is-untruncated-π-finite k (type-Untruncated-π-Finite-Type {l} k A)
+is-untruncated-π-finite-type-Untruncated-π-Finite-Type k = pr2
+```
+
+## Properties
+
+### Untruncated π-finite types are closed under equivalences
+
+```agda
+is-untruncated-π-finite-equiv :
+  {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : UU l2} →
+  A ≃ B → is-untruncated-π-finite k B → is-untruncated-π-finite k A
+is-untruncated-π-finite-equiv zero-ℕ =
+  has-finitely-many-connected-components-equiv'
+pr1 (is-untruncated-π-finite-equiv (succ-ℕ k) e H) =
+  is-untruncated-π-finite-equiv zero-ℕ e (pr1 H)
+pr2 (is-untruncated-π-finite-equiv (succ-ℕ k) e H) a b =
+  is-untruncated-π-finite-equiv k
+    ( equiv-ap e a b)
+    ( pr2 H (map-equiv e a) (map-equiv e b))
+
+is-untruncated-π-finite-equiv' :
+  {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : UU l2} →
+  A ≃ B → is-untruncated-π-finite k A → is-untruncated-π-finite k B
+is-untruncated-π-finite-equiv' k e =
+  is-untruncated-π-finite-equiv k (inv-equiv e)
+```
+
+### Untruncated π-finite types are closed under retracts
+
+```agda
+is-untruncated-π-finite-retract :
+  {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : UU l2} →
+  A retract-of B → is-untruncated-π-finite k B → is-untruncated-π-finite k A
+is-untruncated-π-finite-retract zero-ℕ =
+  has-finitely-many-connected-components-retract
+pr1 (is-untruncated-π-finite-retract (succ-ℕ k) r H) =
+  is-untruncated-π-finite-retract zero-ℕ r
+    ( has-finitely-many-connected-components-is-untruncated-π-finite
+      ( succ-ℕ k)
+      ( H))
+pr2 (is-untruncated-π-finite-retract (succ-ℕ k) r H) x y =
+  is-untruncated-π-finite-retract k
+    ( retract-eq r x y)
+    ( pr2 H (inclusion-retract r x) (inclusion-retract r y))
+```
+
+### Empty types are untruncated π-finite
+
+```agda
+is-untruncated-π-finite-empty : (k : ℕ) → is-untruncated-π-finite k empty
+is-untruncated-π-finite-empty zero-ℕ =
+  has-finitely-many-connected-components-empty
+pr1 (is-untruncated-π-finite-empty (succ-ℕ k)) =
+  is-untruncated-π-finite-empty zero-ℕ
+pr2 (is-untruncated-π-finite-empty (succ-ℕ k)) = ind-empty
+
+empty-Untruncated-π-Finite-Type : (k : ℕ) → Untruncated-π-Finite-Type lzero k
+pr1 (empty-Untruncated-π-Finite-Type k) = empty
+pr2 (empty-Untruncated-π-Finite-Type k) = is-untruncated-π-finite-empty k
+
+is-untruncated-π-finite-is-empty :
+  {l : Level} (k : ℕ) {A : UU l} → is-empty A → is-untruncated-π-finite k A
+is-untruncated-π-finite-is-empty zero-ℕ =
+  has-finitely-many-connected-components-is-empty
+pr1 (is-untruncated-π-finite-is-empty (succ-ℕ k) f) =
+  is-untruncated-π-finite-is-empty zero-ℕ f
+pr2 (is-untruncated-π-finite-is-empty (succ-ℕ k) f) a = ex-falso (f a)
+```
+
+### Contractible types are untruncated π-finite
+
+```agda
+is-untruncated-π-finite-is-contr :
+  {l : Level} (k : ℕ) {A : UU l} → is-contr A → is-untruncated-π-finite k A
+is-untruncated-π-finite-is-contr zero-ℕ =
+  has-finitely-many-connected-components-is-contr
+pr1 (is-untruncated-π-finite-is-contr (succ-ℕ k) H) =
+  is-untruncated-π-finite-is-contr zero-ℕ H
+pr2 (is-untruncated-π-finite-is-contr (succ-ℕ k) H) x y =
+  is-untruncated-π-finite-is-contr k ( is-prop-is-contr H x y)
+
+is-untruncated-π-finite-unit : (k : ℕ) → is-untruncated-π-finite k unit
+is-untruncated-π-finite-unit k =
+  is-untruncated-π-finite-is-contr k is-contr-unit
+
+unit-Untruncated-π-Finite-Type : (k : ℕ) → Untruncated-π-Finite-Type lzero k
+pr1 (unit-Untruncated-π-Finite-Type k) = unit
+pr2 (unit-Untruncated-π-Finite-Type k) = is-untruncated-π-finite-unit k
+```
+
+### Coproducts of untruncated π-finite types are untruncated π-finite
+
+```agda
+is-untruncated-π-finite-coproduct :
+  {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : UU l2} →
+  is-untruncated-π-finite k A → is-untruncated-π-finite k B →
+  is-untruncated-π-finite k (A + B)
+is-untruncated-π-finite-coproduct zero-ℕ =
+  has-finitely-many-connected-components-coproduct
+pr1 (is-untruncated-π-finite-coproduct (succ-ℕ k) H K) =
+  is-untruncated-π-finite-coproduct zero-ℕ (pr1 H) (pr1 K)
+pr2 (is-untruncated-π-finite-coproduct (succ-ℕ k) H K) (inl x) (inl y) =
+  is-untruncated-π-finite-equiv k
+    ( compute-eq-coproduct-inl-inl x y)
+    ( pr2 H x y)
+pr2 (is-untruncated-π-finite-coproduct (succ-ℕ k) H K) (inl x) (inr y) =
+  is-untruncated-π-finite-equiv k
+    ( compute-eq-coproduct-inl-inr x y)
+    ( is-untruncated-π-finite-empty k)
+pr2 (is-untruncated-π-finite-coproduct (succ-ℕ k) H K) (inr x) (inl y) =
+  is-untruncated-π-finite-equiv k
+    ( compute-eq-coproduct-inr-inl x y)
+    ( is-untruncated-π-finite-empty k)
+pr2 (is-untruncated-π-finite-coproduct (succ-ℕ k) H K) (inr x) (inr y) =
+  is-untruncated-π-finite-equiv k
+    ( compute-eq-coproduct-inr-inr x y)
+    ( pr2 K x y)
+
+coproduct-Untruncated-π-Finite-Type :
+  {l1 l2 : Level} (k : ℕ) →
+  Untruncated-π-Finite-Type l1 k →
+  Untruncated-π-Finite-Type l2 k →
+  Untruncated-π-Finite-Type (l1 ⊔ l2) k
+pr1 (coproduct-Untruncated-π-Finite-Type k A B) =
+  (type-Untruncated-π-Finite-Type k A + type-Untruncated-π-Finite-Type k B)
+pr2 (coproduct-Untruncated-π-Finite-Type k A B) =
+  is-untruncated-π-finite-coproduct k
+    ( is-untruncated-π-finite-type-Untruncated-π-Finite-Type k A)
+    ( is-untruncated-π-finite-type-Untruncated-π-Finite-Type k B)
+```
+
+### `Maybe A` of any untruncated π-finite type `A` is untruncated π-finite
+
+```agda
+Maybe-Untruncated-π-Finite-Type :
+  {l : Level} (k : ℕ) →
+  Untruncated-π-Finite-Type l k →
+  Untruncated-π-Finite-Type l k
+Maybe-Untruncated-π-Finite-Type k A =
+  coproduct-Untruncated-π-Finite-Type k A (unit-Untruncated-π-Finite-Type k)
+
+is-untruncated-π-finite-Maybe :
+  {l : Level} (k : ℕ) {A : UU l} →
+  is-untruncated-π-finite k A → is-untruncated-π-finite k (Maybe A)
+is-untruncated-π-finite-Maybe k H =
+  is-untruncated-π-finite-coproduct k H (is-untruncated-π-finite-unit k)
+```
+
+### Any stanadard finite type is untruncated π-finite
+
+```agda
+is-untruncated-π-finite-Fin :
+  (k n : ℕ) → is-untruncated-π-finite k (Fin n)
+is-untruncated-π-finite-Fin k zero-ℕ =
+  is-untruncated-π-finite-empty k
+is-untruncated-π-finite-Fin k (succ-ℕ n) =
+  is-untruncated-π-finite-Maybe k (is-untruncated-π-finite-Fin k n)
+
+Fin-Untruncated-π-Finite-Type :
+  (k : ℕ) (n : ℕ) → Untruncated-π-Finite-Type lzero k
+pr1 (Fin-Untruncated-π-Finite-Type k n) = Fin n
+pr2 (Fin-Untruncated-π-Finite-Type k n) = is-untruncated-π-finite-Fin k n
+```
+
+### Any type equipped with a counting is untruncated π-finite
+
+```agda
+is-untruncated-π-finite-count :
+  {l : Level} (k : ℕ) {A : UU l} → count A → is-untruncated-π-finite k A
+is-untruncated-π-finite-count k (n , e) =
+  is-untruncated-π-finite-equiv' k e (is-untruncated-π-finite-Fin k n)
+```
+
+### Any finite type is untruncated π-finite
+
+```agda
+is-untruncated-π-finite-is-finite :
+  {l : Level} (k : ℕ) {A : UU l} → is-finite A → is-untruncated-π-finite k A
+is-untruncated-π-finite-is-finite k {A} H =
+  apply-universal-property-trunc-Prop H
+    ( is-untruncated-π-finite-Prop k A)
+    ( is-untruncated-π-finite-count k)
+
+π-finite-𝔽 : {l : Level} (k : ℕ) → 𝔽 l → Untruncated-π-Finite-Type l k
+pr1 (π-finite-𝔽 k A) = type-𝔽 A
+pr2 (π-finite-𝔽 k A) = is-untruncated-π-finite-is-finite k (is-finite-type-𝔽 A)
+```
+
+### The type of all `n`-element types in `UU l` is untruncated π-finite
+
+```agda
+is-untruncated-π-finite-UU-Fin :
+  {l : Level} (k n : ℕ) → is-untruncated-π-finite k (UU-Fin l n)
+is-untruncated-π-finite-UU-Fin zero-ℕ n =
+  has-finitely-many-connected-components-UU-Fin n
+pr1 (is-untruncated-π-finite-UU-Fin (succ-ℕ k) n) =
+  is-untruncated-π-finite-UU-Fin zero-ℕ n
+pr2 (is-untruncated-π-finite-UU-Fin (succ-ℕ k) n) x y =
+  is-untruncated-π-finite-equiv k
+    ( equiv-equiv-eq-UU-Fin n x y)
+    ( is-untruncated-π-finite-is-finite k
+      ( is-finite-≃
+        ( is-finite-has-finite-cardinality (n , pr2 x))
+        ( is-finite-has-finite-cardinality (n , pr2 y))))
+```
+
+### Untruncated πₙ₊₁-finite types are untruncated πₙ-finite
+
+```agda
+is-untruncated-π-finite-is-untruncated-π-finite-succ-ℕ :
+  {l : Level} (k : ℕ) {A : UU l} →
+  is-untruncated-π-finite (succ-ℕ k) A → is-untruncated-π-finite k A
+is-untruncated-π-finite-is-untruncated-π-finite-succ-ℕ zero-ℕ H =
+  has-finitely-many-connected-components-is-untruncated-π-finite 1 H
+pr1 (is-untruncated-π-finite-is-untruncated-π-finite-succ-ℕ (succ-ℕ k) H) =
+  has-finitely-many-connected-components-is-untruncated-π-finite
+    ( succ-ℕ (succ-ℕ k))
+    ( H)
+pr2 (is-untruncated-π-finite-is-untruncated-π-finite-succ-ℕ (succ-ℕ k) H) x y =
+  is-untruncated-π-finite-is-untruncated-π-finite-succ-ℕ k (pr2 H x y)
+```
+
+### Untruncated πₙ₊₁-finite types are untruncated π₁-finite
+
+```agda
+is-untruncated-π-finite-one-is-untruncated-π-finite-succ-ℕ :
+  {l : Level} (k : ℕ) {A : UU l} →
+  is-untruncated-π-finite (succ-ℕ k) A → is-untruncated-π-finite 1 A
+is-untruncated-π-finite-one-is-untruncated-π-finite-succ-ℕ zero-ℕ H = H
+is-untruncated-π-finite-one-is-untruncated-π-finite-succ-ℕ (succ-ℕ k) H =
+  is-untruncated-π-finite-one-is-untruncated-π-finite-succ-ℕ k
+    ( is-untruncated-π-finite-is-untruncated-π-finite-succ-ℕ (succ-ℕ k) H)
+```
+
+### Untruncated πₙ-finite sets are finite
+
+```agda
+is-finite-is-untruncated-π-finite :
+  {l : Level} (k : ℕ) {A : UU l} → is-set A →
+  is-untruncated-π-finite k A → is-finite A
+is-finite-is-untruncated-π-finite k H K =
+  is-finite-equiv'
+    ( equiv-unit-trunc-Set (_ , H))
+    ( has-finitely-many-connected-components-is-untruncated-π-finite k K)
+```
+
+### Finite products of untruncated π-finite types are untruncated π-finite
+
+```agda
+is-untruncated-π-finite-Π :
+  {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : A → UU l2} →
+  is-finite A → ((a : A) → is-untruncated-π-finite k (B a)) →
+  is-untruncated-π-finite k ((a : A) → B a)
+is-untruncated-π-finite-Π zero-ℕ =
+  has-finitely-many-connected-components-finite-Π
+pr1 (is-untruncated-π-finite-Π (succ-ℕ k) H K) =
+  is-untruncated-π-finite-Π zero-ℕ H (λ a → pr1 (K a))
+pr2 (is-untruncated-π-finite-Π (succ-ℕ k) H K) f g =
+  is-untruncated-π-finite-equiv k
+    ( equiv-funext)
+    ( is-untruncated-π-finite-Π k H (λ a → pr2 (K a) (f a) (g a)))
+
+Untruncated-π-Finite-Type-Π :
+  {l1 l2 : Level} (k : ℕ) (A : 𝔽 l1)
+  (B : type-𝔽 A → Untruncated-π-Finite-Type l2 k) →
+  Untruncated-π-Finite-Type (l1 ⊔ l2) k
+pr1 (Untruncated-π-Finite-Type-Π k A B) =
+  (x : type-𝔽 A) → (type-Untruncated-π-Finite-Type k (B x))
+pr2 (Untruncated-π-Finite-Type-Π k A B) =
+  is-untruncated-π-finite-Π k
+    ( is-finite-type-𝔽 A)
+    ( λ x → is-untruncated-π-finite-type-Untruncated-π-Finite-Type k (B x))
+```
+
+### Dependent sums of types with finitely many connected components over a `0`-connected base
+
+The total space of a family of types with finitely many connected components
+over a `0`-connected base has finitely many connected components when the based
+[loop spaces](synthetic-homotopy-theory.loop-spaces.md) of the base have
+finitely many connected components.
+
+```agda
+has-finitely-many-connected-components-Σ-is-0-connected :
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
+  is-0-connected A →
+  ((a : A) → has-finitely-many-connected-components (a ＝ a)) →
+  ((x : A) → has-finitely-many-connected-components (B x)) →
+  has-finitely-many-connected-components (Σ A B)
+has-finitely-many-connected-components-Σ-is-0-connected {A = A} {B} C H K =
+  apply-universal-property-trunc-Prop
+    ( is-inhabited-is-0-connected C)
+    ( has-finitely-many-connected-components-Prop (Σ A B))
+    ( α)
+  where
+  α : A → has-finitely-many-connected-components (Σ A B)
+  α a =
+    is-finite-codomain
+      ( K a)
+      ( is-surjective-map-trunc-Set
+        ( fiber-inclusion B a)
+        ( is-surjective-fiber-inclusion C a))
+      ( apply-dependent-universal-property-trunc-Set'
+        ( λ x →
+          set-Prop
+            ( Π-Prop
+              ( type-trunc-Set (Σ A B))
+              ( λ y → is-decidable-Prop (Id-Prop (trunc-Set (Σ A B)) x y))))
+        ( β))
+    where
+    β :
+      (x : Σ A B) (v : type-trunc-Set (Σ A B)) →
+      is-decidable (unit-trunc-Set x ＝ v)
+    β (x , y) =
+      apply-dependent-universal-property-trunc-Set'
+        ( λ u →
+          set-Prop
+            ( is-decidable-Prop
+              ( Id-Prop (trunc-Set (Σ A B)) (unit-trunc-Set (x , y)) u)))
+        ( γ)
+      where
+      γ :
+        (v : Σ A B) →
+        is-decidable ((unit-trunc-Set (x , y)) ＝ (unit-trunc-Set v))
+      γ (x' , y') =
+        is-decidable-equiv
+          ( is-effective-unit-trunc-Set
+            ( Σ A B)
+            ( x , y)
+            ( x' , y'))
+          ( apply-universal-property-trunc-Prop
+            ( mere-eq-is-0-connected C a x)
+            ( is-decidable-Prop
+              ( mere-eq-Prop (x , y) (x' , y')))
+              ( δ))
+        where
+        δ : a ＝ x → is-decidable (mere-eq (x , y) (x' , y'))
+        δ refl =
+          apply-universal-property-trunc-Prop
+            ( mere-eq-is-0-connected C a x')
+            ( is-decidable-Prop
+              ( mere-eq-Prop (a , y) (x' , y')))
+            ( ε)
+          where
+          ε : a ＝ x' → is-decidable (mere-eq (x , y) (x' , y'))
+          ε refl =
+            is-decidable-equiv e
+              ( is-decidable-type-trunc-Prop-is-finite
+                ( is-finite-Σ
+                  ( H a)
+                  ( λ ω → is-finite-is-decidable-Prop (P ω) (d ω))))
+            where
+            ℙ :
+              is-contr
+                ( Σ ( hom-Set (trunc-Set (a ＝ a)) (Prop-Set _))
+                    ( λ h →
+                      ( λ a₁ → h (unit-trunc-Set a₁)) ~
+                      ( λ ω₁ →
+                        trunc-Prop (dependent-identification B ω₁ y y'))))
+            ℙ =
+              universal-property-trunc-Set
+                ( a ＝ a)
+                ( Prop-Set _)
+                ( λ ω → trunc-Prop (dependent-identification B ω y y'))
+
+            P : type-trunc-Set (Id a a) → Prop _
+            P = pr1 (center ℙ)
+
+            compute-P :
+              (ω : a ＝ a) →
+              type-Prop (P (unit-trunc-Set ω)) ≃
+              type-trunc-Prop (dependent-identification B ω y y')
+            compute-P ω = equiv-eq (ap pr1 (pr2 (center ℙ) ω))
+
+            d : (t : type-trunc-Set (a ＝ a)) → is-decidable (type-Prop (P t))
+            d =
+              apply-dependent-universal-property-trunc-Set'
+                ( λ t → set-Prop (is-decidable-Prop (P t)))
+                ( λ ω →
+                  is-decidable-equiv'
+                    ( inv-equiv (compute-P ω))
+                    ( is-decidable-equiv'
+                      ( is-effective-unit-trunc-Set (B a) (tr B ω y) y')
+                      ( has-decidable-equality-is-finite
+                        ( K a)
+                        ( unit-trunc-Set (tr B ω y))
+                        ( unit-trunc-Set y'))))
+
+            f : type-hom-Prop
+                ( trunc-Prop (Σ (type-trunc-Set (Id a a)) (type-Prop ∘ P)))
+                ( mere-eq-Prop {A = Σ A B} (a , y) (a , y'))
+            f t =
+              apply-universal-property-trunc-Prop t
+                ( mere-eq-Prop (a , y) (a , y'))
+                  λ (u , v) →
+                  apply-dependent-universal-property-trunc-Set'
+                    ( λ u' →
+                      hom-set-Set
+                        ( set-Prop (P u'))
+                        ( set-Prop
+                          ( mere-eq-Prop (a , y) (a , y'))))
+                    ( λ ω v' →
+                      apply-universal-property-trunc-Prop
+                        ( map-equiv (compute-P ω) v')
+                        ( mere-eq-Prop (a , y) (a , y'))
+                        ( λ p → unit-trunc-Prop (eq-pair-Σ ω p)))
+                    ( u)
+                    ( v)
+            e :
+              mere-eq {A = Σ A B} (a , y) (a , y') ≃
+              type-trunc-Prop (Σ (type-trunc-Set (Id a a)) (type-Prop ∘ P))
+            e =
+              equiv-iff
+                ( mere-eq-Prop (a , y) (a , y'))
+                ( trunc-Prop (Σ (type-trunc-Set (a ＝ a)) (type-Prop ∘ P)))
+                ( λ t →
+                  apply-universal-property-trunc-Prop t
+                    ( trunc-Prop _)
+                    ( ( λ (ω , r) →
+                        unit-trunc-Prop
+                          { A = Σ (type-trunc-Set (a ＝ a)) (type-Prop ∘ P)}
+                          ( ( unit-trunc-Set ω) ,
+                            ( map-inv-equiv
+                              ( compute-P ω)
+                              ( unit-trunc-Prop r)))) ∘
+                      ( pair-eq-Σ)))
+                ( f)
+```
+
+### Dependent sums of types with finitely many connected components
+
+```agda
+abstract
+  has-finitely-many-connected-components-Σ' :
+    {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : A → UU l2} →
+    (Fin k ≃ type-trunc-Set A) →
+    ((x y : A) → has-finitely-many-connected-components (x ＝ y)) →
+    ((x : A) → has-finitely-many-connected-components (B x)) →
+    has-finitely-many-connected-components (Σ A B)
+  has-finitely-many-connected-components-Σ' zero-ℕ e H K =
+    has-finitely-many-connected-components-is-empty
+      ( is-empty-is-empty-trunc-Set (map-inv-equiv e) ∘ pr1)
+  has-finitely-many-connected-components-Σ' (succ-ℕ k) {A} {B} e H K =
+    apply-universal-property-trunc-Prop
+      ( has-presentation-of-cardinality-has-cardinality-connected-components
+        ( succ-ℕ k)
+        ( unit-trunc-Prop e))
+      ( has-finitely-many-connected-components-Prop (Σ A B))
+      ( α)
+    where
+    α : Σ (Fin (succ-ℕ k) → A) (λ f → is-equiv (unit-trunc-Set ∘ f)) →
+        has-finitely-many-connected-components (Σ A B)
+    α (f , Eηf) =
+      is-finite-equiv
+        ( equiv-trunc-Set g)
+        ( is-finite-equiv'
+          ( equiv-distributive-trunc-coproduct-Set
+            ( Σ (im (f ∘ inl)) (B ∘ pr1))
+            ( Σ (im (f ∘ inr)) (B ∘ pr1)))
+          ( is-finite-coproduct
+            ( has-finitely-many-connected-components-Σ' k
+              ( h)
+              ( λ x y →
+                is-finite-equiv'
+                  ( equiv-trunc-Set
+                    ( equiv-ap-emb
+                      ( pr1 , is-emb-inclusion-subtype ( λ u → trunc-Prop _))))
+                  ( H (pr1 x) (pr1 y)))
+              ( λ x → K (pr1 x)))
+            ( has-finitely-many-connected-components-Σ-is-0-connected
+              ( is-0-connected-im-is-0-connected-domain
+                ( f ∘ inr)
+                ( is-0-connected-unit))
+              ( λ a →
+                has-finitely-many-connected-components-equiv'
+                  ( equiv-Eq-eq-im (f ∘ inr) a a)
+                  ( H (pr1 a) (pr1 a)))
+              ( λ x → K (pr1 x)))))
+      where
+      g : ((Σ (im (f ∘ inl)) (B ∘ pr1)) + (Σ (im (f ∘ inr)) (B ∘ pr1))) ≃
+          Σ A B
+      g =
+        ( equiv-Σ B
+          ( is-coproduct-codomain f
+            ( unit-trunc-Set ∘ f , Eηf)
+            ( refl-htpy))
+          ( λ { (inl x) → id-equiv ; (inr x) → id-equiv})) ∘e
+        ( inv-equiv
+          ( right-distributive-Σ-coproduct
+            ( im (f ∘ inl))
+            ( im (f ∘ inr))
+            ( rec-coproduct (B ∘ pr1) (B ∘ pr1))))
+
+      i : Fin k → type-trunc-Set (im (f ∘ inl))
+      i = unit-trunc-Set ∘ map-unit-im (f ∘ inl)
+
+      is-surjective-i : is-surjective i
+      is-surjective-i =
+        is-surjective-comp
+          ( is-surjective-unit-trunc-Set (im (f ∘ inl)))
+          ( is-surjective-map-unit-im (f ∘ inl))
+
+      is-emb-i : is-emb i
+      is-emb-i =
+        is-emb-top-map-triangle
+          ( (unit-trunc-Set ∘ f) ∘ inl)
+          ( inclusion-trunc-im-Set (f ∘ inl))
+          ( i)
+          ( ( inv-htpy (naturality-unit-trunc-Set (inclusion-im (f ∘ inl)))) ·r
+            ( map-unit-im (f ∘ inl)))
+          ( is-emb-inclusion-trunc-im-Set (f ∘ inl))
+          ( is-emb-comp
+            ( unit-trunc-Set ∘ f)
+            ( inl)
+            ( is-emb-is-equiv Eηf)
+            ( is-emb-inl))
+      h : Fin k ≃ type-trunc-Set (im (f ∘ inl))
+      h = i , (is-equiv-is-emb-is-surjective is-surjective-i is-emb-i)
+```
+
+### Dependent sums of untruncated π-finite types
+
+The dependent sum of a family of untruncated πₙ-finite types over a untruncated
+πₙ₊₁-finite base is untruncated πₙ-finite.
+
+```agda
+has-finitely-many-connected-components-Σ :
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
+  is-untruncated-π-finite 1 A →
+  ((x : A) → has-finitely-many-connected-components (B x)) →
+  has-finitely-many-connected-components (Σ A B)
+has-finitely-many-connected-components-Σ {A = A} {B} H K =
+  apply-universal-property-trunc-Prop
+    ( pr1 H)
+    ( has-finitely-many-connected-components-Prop (Σ A B))
+    ( λ (k , e) →
+      has-finitely-many-connected-components-Σ' k e (λ x y → pr2 H x y) K)
+
+abstract
+  is-untruncated-π-finite-Σ :
+    {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : A → UU l2} →
+    is-untruncated-π-finite (succ-ℕ k) A →
+    ((x : A) → is-untruncated-π-finite k (B x)) →
+    is-untruncated-π-finite k (Σ A B)
+  is-untruncated-π-finite-Σ zero-ℕ =
+    has-finitely-many-connected-components-Σ
+  pr1 (is-untruncated-π-finite-Σ (succ-ℕ k) H K) =
+    has-finitely-many-connected-components-Σ
+      ( is-untruncated-π-finite-one-is-untruncated-π-finite-succ-ℕ (succ-ℕ k) H)
+      ( λ x →
+        has-finitely-many-connected-components-is-untruncated-π-finite
+          ( succ-ℕ k)
+          ( K x))
+  pr2 (is-untruncated-π-finite-Σ (succ-ℕ k) H K) (x , u) (y , v) =
+    is-untruncated-π-finite-equiv k
+      ( equiv-pair-eq-Σ (x , u) (y , v))
+      ( is-untruncated-π-finite-Σ k
+        ( pr2 H x y)
+        ( λ where refl → pr2 (K x) u v))
+
+Untruncated-π-Finite-Type-Σ :
+  {l1 l2 : Level} (k : ℕ) (A : Untruncated-π-Finite-Type l1 (succ-ℕ k))
+  (B :
+    (x : type-Untruncated-π-Finite-Type (succ-ℕ k) A) →
+    Untruncated-π-Finite-Type l2 k) →
+  Untruncated-π-Finite-Type (l1 ⊔ l2) k
+pr1 (Untruncated-π-Finite-Type-Σ k A B) =
+  Σ ( type-Untruncated-π-Finite-Type (succ-ℕ k) A)
+    ( λ x → type-Untruncated-π-Finite-Type k (B x))
+pr2 (Untruncated-π-Finite-Type-Σ k A B) =
+  is-untruncated-π-finite-Σ k
+    ( is-untruncated-π-finite-type-Untruncated-π-Finite-Type (succ-ℕ k) A)
+    ( λ x → is-untruncated-π-finite-type-Untruncated-π-Finite-Type k (B x))
+```
+
+## See also
+
+- [π-finite types](univalent-combinatorics.pi-finite-types.md)
+- [Unbounded π-finite types](univalent-combinatorics.unbounded-pi-finite-types.md)