From 37e8fa42a40c74c05f750d091fb3af4fcaf97db1 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 6 Jan 2025 16:53:52 +0100
Subject: [PATCH] =?UTF-8?q?Unbounded=20=CF=80-finite=20types=20(#1168)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Defines unbounded π-finite types and repeats the proofs that are already
done for π-finite types. This includes
- Unbounded π-finite types are closed under equivalences and retracts.
- Truncated π-finite types are unbounded π-finite.
- Unbounded π-finite types are types that are πₙ-finite for all $n$.
- Unbounded π-finite types are closed under coproducts.
- Unbounded π-finite types are closed under finite products.
- Unbounded π-finite types are closed under dependent sums.
---
 references.bib                                |  10 +
 .../functoriality-set-truncation.lagda.md     |  10 +
 src/polytopes/abstract-polytopes.lagda.md     |   4 +-
 src/univalent-combinatorics.lagda.md          |   6 +
 .../equality-finite-types.lagda.md            |   9 +-
 ...initely-many-connected-components.lagda.md |  98 ++++
 .../pi-finite-types.lagda.md                  | 143 ++----
 .../retracts-of-finite-types.lagda.md         |   5 +-
 .../standard-finite-types.lagda.md            |   1 -
 .../truncated-pi-finite-types.lagda.md        | 109 +++++
 .../unbounded-pi-finite-types.lagda.md        | 457 ++++++++++++++++++
 11 files changed, 752 insertions(+), 100 deletions(-)
 create mode 100644 src/univalent-combinatorics/truncated-pi-finite-types.lagda.md
 create mode 100644 src/univalent-combinatorics/unbounded-pi-finite-types.lagda.md

diff --git a/references.bib b/references.bib
index 9a25a11681..aef4fe98c3 100644
--- a/references.bib
+++ b/references.bib
@@ -28,6 +28,16 @@ @article{AKS15
   langid      = {english}
 }
 
+@misc{Anel24,
+  title         = {The category of $\pi$-finite spaces},
+  author        = {Mathieu Anel},
+  year          = {2024},
+  eprint        = {2107.02082},
+  archiveprefix = {arXiv},
+  eprintclass   = {math},
+  primaryclass  = {math.CT}
+}
+
 @article{AL19,
   title       = {Displayed Categories},
   author      = {Ahrens, Benedikt and {{LeFanu}} Lumsdaine, Peter},
diff --git a/src/foundation/functoriality-set-truncation.lagda.md b/src/foundation/functoriality-set-truncation.lagda.md
index c0539827f8..6e1fb2db8d 100644
--- a/src/foundation/functoriality-set-truncation.lagda.md
+++ b/src/foundation/functoriality-set-truncation.lagda.md
@@ -13,6 +13,7 @@ open import foundation.functoriality-truncation
 open import foundation.images
 open import foundation.injective-maps
 open import foundation.propositional-truncations
+open import foundation.retracts-of-types
 open import foundation.set-truncations
 open import foundation.sets
 open import foundation.slice
@@ -165,6 +166,15 @@ module _
         ( htpy-map-equiv-trunc-Σ-Set)
 ```
 
+### The set truncation functor preserves retracts
+
+```agda
+retract-trunc-Set :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+  (A retract-of B) → (type-trunc-Set A) retract-of (type-trunc-Set B)
+retract-trunc-Set = retract-of-trunc-retract-of
+```
+
 ### The set truncation functor preserves injective maps
 
 ```agda
diff --git a/src/polytopes/abstract-polytopes.lagda.md b/src/polytopes/abstract-polytopes.lagda.md
index 85a5bacfab..6e9acff90a 100644
--- a/src/polytopes/abstract-polytopes.lagda.md
+++ b/src/polytopes/abstract-polytopes.lagda.md
@@ -13,6 +13,7 @@ open import elementary-number-theory.natural-numbers
 open import foundation.binary-relations
 open import foundation.cartesian-product-types
 open import foundation.contractible-types
+open import foundation.dependent-pair-types
 open import foundation.disjunction
 open import foundation.identity-types
 open import foundation.propositional-truncations
@@ -25,7 +26,8 @@ open import foundation.universe-levels
 open import order-theory.finitely-graded-posets
 open import order-theory.posets
 
-open import univalent-combinatorics
+open import univalent-combinatorics.finite-types
+open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>
diff --git a/src/univalent-combinatorics.lagda.md b/src/univalent-combinatorics.lagda.md
index d7d2896487..907d4b8990 100644
--- a/src/univalent-combinatorics.lagda.md
+++ b/src/univalent-combinatorics.lagda.md
@@ -1,5 +1,9 @@
 # Univalent combinatorics
 
+```agda
+{-# OPTIONS --guardedness #-}
+```
+
 ## Idea
 
 Univalent combinatorics is the study of finite univalent mathematics. Finiteness
@@ -103,7 +107,9 @@ 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
 open import univalent-combinatorics.universal-property-standard-finite-types public
 open import univalent-combinatorics.unlabeled-partitions public
diff --git a/src/univalent-combinatorics/equality-finite-types.lagda.md b/src/univalent-combinatorics/equality-finite-types.lagda.md
index acce1ec73c..c5811f2e6b 100644
--- a/src/univalent-combinatorics/equality-finite-types.lagda.md
+++ b/src/univalent-combinatorics/equality-finite-types.lagda.md
@@ -63,14 +63,17 @@ has-decidable-equality-has-cardinality {l1} {X} k H =
 ```agda
 abstract
   is-finite-eq :
-    {l1 : Level} {X : UU l1} →
+    {l : Level} {X : UU l} →
     has-decidable-equality X → {x y : X} → is-finite (Id x y)
   is-finite-eq d {x} {y} = is-finite-count (count-eq d x y)
 
+is-finite-eq-is-finite :
+    {l : Level} {X : UU l} → is-finite X → {x y : X} → is-finite (x ＝ y)
+is-finite-eq-is-finite H = is-finite-eq (has-decidable-equality-is-finite H)
+
 is-finite-eq-𝔽 :
   {l : Level} → (X : 𝔽 l) {x y : type-𝔽 X} → is-finite (x ＝ y)
-is-finite-eq-𝔽 X =
-  is-finite-eq (has-decidable-equality-is-finite (is-finite-type-𝔽 X))
+is-finite-eq-𝔽 X = is-finite-eq-is-finite (is-finite-type-𝔽 X)
 
 Id-𝔽 : {l : Level} → (X : 𝔽 l) (x y : type-𝔽 X) → 𝔽 l
 pr1 (Id-𝔽 X x y) = Id x y
diff --git a/src/univalent-combinatorics/finitely-many-connected-components.lagda.md b/src/univalent-combinatorics/finitely-many-connected-components.lagda.md
index 933c5491c8..093bc92fde 100644
--- a/src/univalent-combinatorics/finitely-many-connected-components.lagda.md
+++ b/src/univalent-combinatorics/finitely-many-connected-components.lagda.md
@@ -10,17 +10,26 @@ module univalent-combinatorics.finitely-many-connected-components where
 open import elementary-number-theory.natural-numbers
 
 open import foundation.0-connected-types
+open import foundation.contractible-types
+open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.equivalences
+open import foundation.function-types
 open import foundation.functoriality-set-truncation
 open import foundation.mere-equivalences
 open import foundation.propositions
+open import foundation.retracts-of-types
 open import foundation.set-truncations
 open import foundation.sets
+open import foundation.unit-type
 open import foundation.universe-levels
 
+open import univalent-combinatorics.coproduct-types
+open import univalent-combinatorics.dependent-function-types
+open import univalent-combinatorics.distributivity-of-set-truncation-over-finite-products
 open import univalent-combinatorics.finite-types
+open import univalent-combinatorics.retracts-of-finite-types
 open import univalent-combinatorics.standard-finite-types
 ```
 
@@ -46,6 +55,11 @@ has-finitely-many-connected-components : {l : Level} → UU l → UU l
 has-finitely-many-connected-components A =
   type-Prop (has-finitely-many-connected-components-Prop A)
 
+is-prop-has-finitely-many-connected-components :
+  {l : Level} {X : UU l} → is-prop (has-finitely-many-connected-components X)
+is-prop-has-finitely-many-connected-components {X = X} =
+  is-prop-type-Prop (has-finitely-many-connected-components-Prop X)
+
 number-of-connected-components :
   {l : Level} {X : UU l} → has-finitely-many-connected-components X → ℕ
 number-of-connected-components H = number-of-elements-is-finite H
@@ -93,6 +107,20 @@ module _
     is-finite-equiv' (equiv-trunc-Set e)
 ```
 
+### Having finitely many connected components is invariant under retracts
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (r : A retract-of B)
+  where
+
+  has-finitely-many-connected-components-retract :
+    has-finitely-many-connected-components B →
+    has-finitely-many-connected-components A
+  has-finitely-many-connected-components-retract =
+    is-finite-retract (retract-trunc-Set r)
+```
+
 ### Empty types have finitely many connected components
 
 ```agda
@@ -100,6 +128,40 @@ has-finitely-many-connected-components-is-empty :
   {l : Level} {A : UU l} → is-empty A → has-finitely-many-connected-components A
 has-finitely-many-connected-components-is-empty f =
   is-finite-is-empty (is-empty-trunc-Set f)
+
+has-finitely-many-connected-components-empty :
+  has-finitely-many-connected-components empty
+has-finitely-many-connected-components-empty =
+  has-finitely-many-connected-components-is-empty id
+```
+
+### Contractible types have finitely many connected components
+
+```agda
+has-finitely-many-connected-components-is-contr :
+  {l : Level} {A : UU l} →
+  is-contr A → has-finitely-many-connected-components A
+has-finitely-many-connected-components-is-contr H =
+  is-finite-is-contr (is-contr-trunc-Set H)
+
+has-finitely-many-connected-components-unit :
+  has-finitely-many-connected-components unit
+has-finitely-many-connected-components-unit =
+  has-finitely-many-connected-components-is-contr is-contr-unit
+```
+
+### Coproducts of types with finitely many connected components
+
+```agda
+has-finitely-many-connected-components-coproduct :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+  has-finitely-many-connected-components A →
+  has-finitely-many-connected-components B →
+  has-finitely-many-connected-components (A + B)
+has-finitely-many-connected-components-coproduct H K =
+  is-finite-equiv'
+    ( equiv-distributive-trunc-coproduct-Set _ _)
+    ( is-finite-coproduct H K)
 ```
 
 ### Any `0`-connected type has finitely many connected components
@@ -111,6 +173,16 @@ has-finitely-many-connected-components-is-0-connected :
 has-finitely-many-connected-components-is-0-connected = is-finite-is-contr
 ```
 
+### Finite types have finitely many connected components
+
+```agda
+has-finitely-many-connected-components-is-finite :
+  {l : Level} {A : UU l} →
+  is-finite A → has-finitely-many-connected-components A
+has-finitely-many-connected-components-is-finite {A = A} H =
+  is-finite-equiv (equiv-unit-trunc-Set (A , is-set-is-finite H)) H
+```
+
 ### Sets with finitely many connected components are finite
 
 ```agda
@@ -121,6 +193,32 @@ is-finite-has-finitely-many-connected-components H =
   is-finite-equiv' (equiv-unit-trunc-Set (_ , H))
 ```
 
+### The type of all `n`-element types in `UU l` has finitely many connected components
+
+```agda
+has-finitely-many-connected-components-UU-Fin :
+  {l : Level} (n : ℕ) → has-finitely-many-connected-components (UU-Fin l n)
+has-finitely-many-connected-components-UU-Fin n =
+  has-finitely-many-connected-components-is-0-connected
+    ( is-0-connected-UU-Fin n)
+```
+
+### Finite products of types with finitely many connected components
+
+```agda
+has-finitely-many-connected-components-finite-Π :
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
+  is-finite A →
+  ((a : A) → has-finitely-many-connected-components (B a)) →
+  has-finitely-many-connected-components ((a : A) → B a)
+has-finitely-many-connected-components-finite-Π {B = B} H K =
+  is-finite-equiv'
+    ( equiv-distributive-trunc-Π-is-finite-Set B H)
+    ( is-finite-Π H K)
+```
+
 ## See also
 
 - [Kuratowski finite sets](univalent-combinatorics.kuratowski-finite-sets.md)
+- [π-finite types](univalent-combinatorics.pi-finite-types.md)
+- [Unbounded π-finite types](univalent-combinatorics.unbounded-pi-finite-types.md)
diff --git a/src/univalent-combinatorics/pi-finite-types.lagda.md b/src/univalent-combinatorics/pi-finite-types.lagda.md
index f066e45870..41814ae2aa 100644
--- a/src/univalent-combinatorics/pi-finite-types.lagda.md
+++ b/src/univalent-combinatorics/pi-finite-types.lagda.md
@@ -16,7 +16,6 @@ open import foundation.coproduct-types
 open import foundation.decidable-propositions
 open import foundation.decidable-types
 open import foundation.dependent-identifications
-open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.empty-types
 open import foundation.equality-coproduct-types
@@ -32,18 +31,16 @@ open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.maybe
 open import foundation.mere-equality
-open import foundation.mere-equivalences
 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.truncated-types
-open import foundation.truncation-levels
 open import foundation.type-arithmetic-coproduct-types
 open import foundation.unit-type
 open import foundation.univalence
@@ -52,9 +49,7 @@ open import foundation.whiskering-homotopies-composition
 
 open import univalent-combinatorics.coproduct-types
 open import univalent-combinatorics.counting
-open import univalent-combinatorics.dependent-function-types
 open import univalent-combinatorics.dependent-pair-types
-open import univalent-combinatorics.distributivity-of-set-truncation-over-finite-products
 open import univalent-combinatorics.equality-finite-types
 open import univalent-combinatorics.finite-types
 open import univalent-combinatorics.finitely-many-connected-components
@@ -69,28 +64,12 @@ 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
+{{#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.
 
-## Definition
-
-### 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)
-```
+## Definitions
 
 ### π-finite types
 
@@ -135,10 +114,10 @@ has-finitely-many-connected-components-is-π-finite (succ-ℕ k) H = pr1 H
 
 ```agda
 is-π-finite-equiv :
-  {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : UU l2} (e : A ≃ B) →
-  is-π-finite k B → is-π-finite k A
-is-π-finite-equiv zero-ℕ e H =
-  is-finite-equiv' (equiv-trunc-Set e) H
+  {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
@@ -146,51 +125,57 @@ pr2 (is-π-finite-equiv (succ-ℕ k) e H) 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} (e : A ≃ B) →
-  is-π-finite k A → is-π-finite k B
+  {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)
 ```
 
-### The empty type is π-finite
+### π-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-ℕ =
-  is-finite-equiv equiv-unit-trunc-empty-Set is-finite-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
-```
 
-### Any empty type is π-finite
-
-```agda
 is-π-finite-is-empty :
   {l : Level} (k : ℕ) {A : UU l} → is-empty A → is-π-finite k A
-is-π-finite-is-empty zero-ℕ f =
-  is-finite-is-empty (is-empty-trunc-Set f)
+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)
 ```
 
-### Any contractible type is π-finite
+### 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-ℕ H =
-  is-finite-is-contr (is-contr-trunc-Set H)
+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)
-```
-
-### The unit type is π-finite
 
-```agda
 is-π-finite-unit : (k : ℕ) → is-π-finite k unit
 is-π-finite-unit k = is-π-finite-is-contr k is-contr-unit
 
@@ -206,10 +191,8 @@ 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-ℕ H K =
-  is-finite-equiv'
-    ( equiv-distributive-trunc-coproduct-Set _ _)
-    ( is-finite-coproduct H K)
+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) =
@@ -300,8 +283,7 @@ pr2 (π-finite-𝔽 k A) = is-π-finite-is-finite k (is-finite-type-𝔽 A)
 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-is-0-connected
-    ( is-0-connected-UU-Fin 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 =
@@ -309,8 +291,8 @@ pr2 (is-π-finite-UU-Fin (succ-ℕ k) n) x y =
     ( 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-finite-has-finite-cardinality (n , pr2 x))
+        ( is-finite-has-finite-cardinality (n , pr2 y))))
 ```
 
 ### πₙ₊₁-finite types are πₙ-finite
@@ -351,34 +333,6 @@ is-finite-is-π-finite k H K =
     ( has-finitely-many-connected-components-is-π-finite k K)
 ```
 
-### πₙ-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)
-```
-
 ### Finite products of π-finite types are π-finite
 
 ```agda
@@ -386,11 +340,10 @@ 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-ℕ {A} {B} H K =
-  is-finite-equiv'
-    ( equiv-distributive-trunc-Π-is-finite-Set B H)
-    ( is-finite-Π H K)
-pr1 (is-π-finite-Π (succ-ℕ k) H K) = is-π-finite-Π zero-ℕ H (λ a → pr1 (K 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)
@@ -552,6 +505,7 @@ has-finitely-many-connected-components-Σ-is-0-connected {A = A} {B} C H K =
                     ( trunc-Prop _)
                     ( ( λ (ω , r) →
                         unit-trunc-Prop
+                          { A = Σ (type-trunc-Set (a ＝ a)) (type-Prop ∘ P)}
                           ( ( unit-trunc-Set ω) ,
                             ( map-inv-equiv
                               ( compute-P ω)
@@ -604,10 +558,10 @@ abstract
               ( 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))))
+              ( λ 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))) ≃
@@ -700,6 +654,11 @@ pr2 (π-Finite-Σ k A B) =
     ( λ x → is-π-finite-type-π-Finite k (B x))
 ```
 
+## See also
+
+- [Truncated π-finite types](univalent-combinatorics.truncated-pi-finite-types.md)
+- [Unbounded π-finite types](univalent-combinatorics.unbounded-pi-finite-types.md)
+
 ## External links
 
 - [pi-finite type](https://ncatlab.org/nlab/show/pi-finite+type) at $n$Lab
diff --git a/src/univalent-combinatorics/retracts-of-finite-types.lagda.md b/src/univalent-combinatorics/retracts-of-finite-types.lagda.md
index f12270336a..d7b3d888e4 100644
--- a/src/univalent-combinatorics/retracts-of-finite-types.lagda.md
+++ b/src/univalent-combinatorics/retracts-of-finite-types.lagda.md
@@ -18,7 +18,6 @@ open import foundation.functoriality-propositional-truncation
 open import foundation.injective-maps
 open import foundation.retractions
 open import foundation.retracts-of-types
-open import foundation.sets
 open import foundation.universe-levels
 
 open import univalent-combinatorics.counting
@@ -93,7 +92,7 @@ count-retract (pair i R) e =
 
 abstract
   is-finite-retract :
-    {l1 l2 : Level} {A : UU l1} {B : UU l2} → A retract-of B →
-    is-finite B → is-finite A
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+    A retract-of B → is-finite B → is-finite A
   is-finite-retract R = map-trunc-Prop (count-retract R)
 ```
diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md
index b581beeac5..c0e169d25e 100644
--- a/src/univalent-combinatorics/standard-finite-types.lagda.md
+++ b/src/univalent-combinatorics/standard-finite-types.lagda.md
@@ -34,7 +34,6 @@ open import foundation.noncontractible-types
 open import foundation.preunivalent-type-families
 open import foundation.raising-universe-levels
 open import foundation.retractions
-open import foundation.sections
 open import foundation.sets
 open import foundation.transport-along-identifications
 open import foundation.unit-type
diff --git a/src/univalent-combinatorics/truncated-pi-finite-types.lagda.md b/src/univalent-combinatorics/truncated-pi-finite-types.lagda.md
new file mode 100644
index 0000000000..aef946deb7
--- /dev/null
+++ b/src/univalent-combinatorics/truncated-pi-finite-types.lagda.md
@@ -0,0 +1,109 @@
+# 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
new file mode 100644
index 0000000000..56e7c6c026
--- /dev/null
+++ b/src/univalent-combinatorics/unbounded-pi-finite-types.lagda.md
@@ -0,0 +1,457 @@
+# Unbounded π-finite types
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module univalent-combinatorics.unbounded-pi-finite-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.cartesian-product-types
+open import foundation.contractible-types
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.equality-coproduct-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.maybe
+open import foundation.retracts-of-types
+open import foundation.set-truncations
+open import foundation.sets
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import univalent-combinatorics.counting
+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.function-types
+open import univalent-combinatorics.pi-finite-types
+open import univalent-combinatorics.standard-finite-types
+open import univalent-combinatorics.truncated-pi-finite-types
+```
+
+</details>
+
+## Idea
+
+A type is
+{{#concept "unbounded π-finite" Disambiguation="type" Agda=is-unbounded-π-finite Agda=Unbounded-Unbounded-π-Finite-Type}}
+if it has [finitely](univalent-combinatorics.finite-types.md) many
+[connected components](foundation.connected-components.md) and all of its
+homotopy groups at all base points and all dimensions are finite. Unbounded
+π-finiteness can be understood as an ∞-dimensional analogue of
+[Kuratowski finitneness](univalent-combinatorics.kuratowski-finite-sets.md)
+{{#cite Anel24}}.
+
+## Definitions
+
+### The predicate on types of being unbounded π-finite
+
+```agda
+record is-unbounded-π-finite {l : Level} (X : UU l) : UU l
+  where
+  coinductive
+  field
+    has-finitely-many-connected-components-is-unbounded-π-finite :
+      has-finitely-many-connected-components X
+
+    is-unbounded-π-finite-Id-is-unbounded-π-finite :
+      (x y : X) → is-unbounded-π-finite (x ＝ y)
+
+open is-unbounded-π-finite public
+```
+
+### The type of unbounded π-finite types
+
+```agda
+Unbounded-π-Finite-Type : (l : Level) → UU (lsuc l)
+Unbounded-π-Finite-Type l = Σ (UU l) (is-unbounded-π-finite)
+
+module _
+  {l : Level} (X : Unbounded-π-Finite-Type l)
+  where
+
+  type-Unbounded-π-Finite-Type : UU l
+  type-Unbounded-π-Finite-Type = pr1 X
+
+  is-unbounded-π-finite-Unbounded-π-Finite-Type :
+    is-unbounded-π-finite type-Unbounded-π-Finite-Type
+  is-unbounded-π-finite-Unbounded-π-Finite-Type = pr2 X
+
+  has-finitely-many-connected-components-Unbounded-π-Finite-Type :
+    has-finitely-many-connected-components type-Unbounded-π-Finite-Type
+  has-finitely-many-connected-components-Unbounded-π-Finite-Type =
+    has-finitely-many-connected-components-is-unbounded-π-finite
+      ( is-unbounded-π-finite-Unbounded-π-Finite-Type)
+
+  is-unbounded-π-finite-Id-Unbounded-π-Finite-Type :
+    (x y : type-Unbounded-π-Finite-Type) → is-unbounded-π-finite (x ＝ y)
+  is-unbounded-π-finite-Id-Unbounded-π-Finite-Type =
+    is-unbounded-π-finite-Id-is-unbounded-π-finite
+      ( is-unbounded-π-finite-Unbounded-π-Finite-Type)
+```
+
+## Properties
+
+### Characterizing equality of unbounded π-finiteness
+
+```agda
+module _
+  {l : Level} {X : UU l}
+  where
+
+  Eq-is-unbounded-π-finite :
+    (p q : is-unbounded-π-finite X) → UU l
+  Eq-is-unbounded-π-finite p q =
+    ( has-finitely-many-connected-components-is-unbounded-π-finite p ＝
+      has-finitely-many-connected-components-is-unbounded-π-finite q) ×
+    ( (x y : X) →
+      is-unbounded-π-finite-Id-is-unbounded-π-finite p x y ＝
+      is-unbounded-π-finite-Id-is-unbounded-π-finite q x y)
+
+  refl-Eq-is-unbounded-π-finite :
+    (p : is-unbounded-π-finite X) → Eq-is-unbounded-π-finite p p
+  refl-Eq-is-unbounded-π-finite p = (refl , λ x y → refl)
+
+  Eq-eq-is-unbounded-π-finite :
+    (p q : is-unbounded-π-finite X) → p ＝ q → Eq-is-unbounded-π-finite p q
+  Eq-eq-is-unbounded-π-finite p .p refl = refl-Eq-is-unbounded-π-finite p
+```
+
+It remains to show that `Eq-is-unbounded-π-finite` defines an identity system on
+`is-unbounded-π-finite`.
+
+### Unbounded π-finite types are closed under equivalences
+
+```agda
+is-unbounded-π-finite-equiv :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B) →
+  is-unbounded-π-finite B → is-unbounded-π-finite A
+is-unbounded-π-finite-equiv e H =
+  λ where
+  .has-finitely-many-connected-components-is-unbounded-π-finite →
+    has-finitely-many-connected-components-equiv' e
+      ( has-finitely-many-connected-components-is-unbounded-π-finite H)
+  .is-unbounded-π-finite-Id-is-unbounded-π-finite x y →
+    is-unbounded-π-finite-equiv
+      ( equiv-ap e x y)
+      ( is-unbounded-π-finite-Id-is-unbounded-π-finite H
+        ( map-equiv e x)
+        ( map-equiv e y))
+
+is-unbounded-π-finite-equiv' :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B) →
+  is-unbounded-π-finite A → is-unbounded-π-finite B
+is-unbounded-π-finite-equiv' e = is-unbounded-π-finite-equiv (inv-equiv e)
+```
+
+### Unbounded π-finite types are closed under retracts
+
+```agda
+is-unbounded-π-finite-retract :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+  A retract-of B → is-unbounded-π-finite B → is-unbounded-π-finite A
+is-unbounded-π-finite-retract r H =
+  λ where
+  .has-finitely-many-connected-components-is-unbounded-π-finite →
+    has-finitely-many-connected-components-retract r
+      ( has-finitely-many-connected-components-is-unbounded-π-finite H)
+  .is-unbounded-π-finite-Id-is-unbounded-π-finite x y →
+    is-unbounded-π-finite-retract
+      ( retract-eq r x y)
+      ( is-unbounded-π-finite-Id-is-unbounded-π-finite H
+        ( inclusion-retract r x)
+        ( inclusion-retract r y))
+```
+
+### Empty types are unbounded π-finite
+
+```agda
+is-unbounded-π-finite-empty : is-unbounded-π-finite empty
+is-unbounded-π-finite-empty =
+  λ where
+  .has-finitely-many-connected-components-is-unbounded-π-finite →
+    has-finitely-many-connected-components-empty
+  .is-unbounded-π-finite-Id-is-unbounded-π-finite ()
+
+empty-Unbounded-π-Finite-Type : Unbounded-π-Finite-Type lzero
+empty-Unbounded-π-Finite-Type = empty , is-unbounded-π-finite-empty
+
+is-unbounded-π-finite-is-empty :
+  {l : Level} {A : UU l} → is-empty A → is-unbounded-π-finite A
+is-unbounded-π-finite-is-empty f =
+  λ where
+  .has-finitely-many-connected-components-is-unbounded-π-finite →
+    has-finitely-many-connected-components-is-empty f
+  .is-unbounded-π-finite-Id-is-unbounded-π-finite → ex-falso ∘ f
+```
+
+### Contractible types are unbounded π-finite
+
+```agda
+is-unbounded-π-finite-is-contr :
+  {l : Level} {A : UU l} → is-contr A → is-unbounded-π-finite A
+is-unbounded-π-finite-is-contr H =
+  λ where
+  .has-finitely-many-connected-components-is-unbounded-π-finite →
+    has-finitely-many-connected-components-is-contr H
+  .is-unbounded-π-finite-Id-is-unbounded-π-finite x y →
+    is-unbounded-π-finite-is-contr (is-prop-is-contr H x y)
+
+is-unbounded-π-finite-unit : is-unbounded-π-finite unit
+is-unbounded-π-finite-unit = is-unbounded-π-finite-is-contr is-contr-unit
+
+unit-Unbounded-π-Finite-Type : Unbounded-π-Finite-Type lzero
+unit-Unbounded-π-Finite-Type = unit , is-unbounded-π-finite-unit
+```
+
+### Coproducts of unbounded π-finite types are unbounded π-finite
+
+```agda
+is-unbounded-π-finite-coproduct :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+  is-unbounded-π-finite A →
+  is-unbounded-π-finite B →
+  is-unbounded-π-finite (A + B)
+is-unbounded-π-finite-coproduct H K =
+  λ where
+  .has-finitely-many-connected-components-is-unbounded-π-finite →
+    has-finitely-many-connected-components-coproduct
+      ( has-finitely-many-connected-components-is-unbounded-π-finite H)
+      ( has-finitely-many-connected-components-is-unbounded-π-finite K)
+  .is-unbounded-π-finite-Id-is-unbounded-π-finite (inl x) (inl y) →
+    is-unbounded-π-finite-equiv
+      ( compute-eq-coproduct-inl-inl x y)
+      ( is-unbounded-π-finite-Id-is-unbounded-π-finite H x y)
+  .is-unbounded-π-finite-Id-is-unbounded-π-finite (inl x) (inr y) →
+    is-unbounded-π-finite-equiv
+      ( compute-eq-coproduct-inl-inr x y)
+      ( is-unbounded-π-finite-empty)
+  .is-unbounded-π-finite-Id-is-unbounded-π-finite (inr x) (inl y) →
+    is-unbounded-π-finite-equiv
+      ( compute-eq-coproduct-inr-inl x y)
+      ( is-unbounded-π-finite-empty)
+  .is-unbounded-π-finite-Id-is-unbounded-π-finite (inr x) (inr y) →
+    is-unbounded-π-finite-equiv
+      ( compute-eq-coproduct-inr-inr x y)
+      ( is-unbounded-π-finite-Id-is-unbounded-π-finite K x y)
+
+coproduct-Unbounded-π-Finite-Type :
+  {l1 l2 : Level} →
+  Unbounded-π-Finite-Type l1 →
+  Unbounded-π-Finite-Type l2 →
+  Unbounded-π-Finite-Type (l1 ⊔ l2)
+pr1 (coproduct-Unbounded-π-Finite-Type A B) =
+  (type-Unbounded-π-Finite-Type A + type-Unbounded-π-Finite-Type B)
+pr2 (coproduct-Unbounded-π-Finite-Type A B) =
+  is-unbounded-π-finite-coproduct
+    ( is-unbounded-π-finite-Unbounded-π-Finite-Type A)
+    ( is-unbounded-π-finite-Unbounded-π-Finite-Type B)
+```
+
+### `Maybe A` of any unbounded π-finite type `A` is unbounded π-finite
+
+```agda
+Maybe-Unbounded-π-Finite-Type :
+  {l : Level} → Unbounded-π-Finite-Type l → Unbounded-π-Finite-Type l
+Maybe-Unbounded-π-Finite-Type A =
+  coproduct-Unbounded-π-Finite-Type A unit-Unbounded-π-Finite-Type
+
+is-unbounded-π-finite-Maybe :
+  {l : Level} {A : UU l} →
+  is-unbounded-π-finite A → is-unbounded-π-finite (Maybe A)
+is-unbounded-π-finite-Maybe H =
+  is-unbounded-π-finite-coproduct H is-unbounded-π-finite-unit
+```
+
+### The standard finite types are unbounded π-finite
+
+```agda
+is-unbounded-π-finite-Fin :
+  (n : ℕ) → is-unbounded-π-finite (Fin n)
+is-unbounded-π-finite-Fin zero-ℕ =
+  is-unbounded-π-finite-empty
+is-unbounded-π-finite-Fin (succ-ℕ n) =
+  is-unbounded-π-finite-Maybe (is-unbounded-π-finite-Fin n)
+
+Fin-Unbounded-π-Finite-Type : (n : ℕ) → Unbounded-π-Finite-Type lzero
+pr1 (Fin-Unbounded-π-Finite-Type n) = Fin n
+pr2 (Fin-Unbounded-π-Finite-Type n) = is-unbounded-π-finite-Fin n
+```
+
+### Any type equipped with a counting is unbounded π-finite
+
+```agda
+is-unbounded-π-finite-count :
+  {l : Level} {A : UU l} → count A → is-unbounded-π-finite A
+is-unbounded-π-finite-count (n , e) =
+  is-unbounded-π-finite-equiv' e (is-unbounded-π-finite-Fin n)
+```
+
+### Any finite type is unbounded π-finite
+
+```agda
+is-unbounded-π-finite-is-finite :
+  {l : Level} {A : UU l} → is-finite A → is-unbounded-π-finite A
+is-unbounded-π-finite-is-finite {A = A} H =
+  λ where
+  .has-finitely-many-connected-components-is-unbounded-π-finite →
+    has-finitely-many-connected-components-is-finite H
+  .is-unbounded-π-finite-Id-is-unbounded-π-finite x y →
+    is-unbounded-π-finite-is-finite (is-finite-eq-is-finite H)
+
+unbounded-π-finite-𝔽 : {l : Level} → 𝔽 l → Unbounded-π-Finite-Type l
+unbounded-π-finite-𝔽 A =
+  ( type-𝔽 A , is-unbounded-π-finite-is-finite (is-finite-type-𝔽 A))
+```
+
+### The type of all `n`-element types in `UU l` is unbounded π-finite
+
+```agda
+is-unbounded-π-finite-UU-Fin :
+  {l : Level} (n : ℕ) → is-unbounded-π-finite (UU-Fin l n)
+is-unbounded-π-finite-UU-Fin n =
+  λ where
+  .has-finitely-many-connected-components-is-unbounded-π-finite →
+    has-finitely-many-connected-components-UU-Fin n
+  .is-unbounded-π-finite-Id-is-unbounded-π-finite x y →
+    is-unbounded-π-finite-equiv
+      ( equiv-equiv-eq-UU-Fin n x y)
+      ( is-unbounded-π-finite-is-finite
+        ( is-finite-≃
+          ( is-finite-has-finite-cardinality (n , pr2 x))
+          ( is-finite-has-finite-cardinality (n , pr2 y))))
+```
+
+### Unbounded π-finite sets are finite
+
+```agda
+is-finite-is-unbounded-π-finite :
+  {l : Level} {A : UU l} → is-set A → is-unbounded-π-finite A → is-finite A
+is-finite-is-unbounded-π-finite H K =
+  is-finite-equiv'
+    ( equiv-unit-trunc-Set (_ , H))
+    ( has-finitely-many-connected-components-is-unbounded-π-finite K)
+```
+
+### Truncated π-finite types are unbounded π-finite
+
+```agda
+is-unbounded-π-finite-is-truncated-π-finite :
+  {l : Level} (k : ℕ) {A : UU l} →
+  is-truncated-π-finite k A → is-unbounded-π-finite A
+is-unbounded-π-finite-is-truncated-π-finite zero-ℕ =
+  is-unbounded-π-finite-is-finite
+is-unbounded-π-finite-is-truncated-π-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)
+```
+
+### Unbounded π-finite types are types that are πₙ-finite for all `n`
+
+```agda
+is-unbounded-π-finite-Id-is-unbounded-π-finite' :
+  {l : Level} {A : UU l} →
+  ((k : ℕ) → is-π-finite k A) →
+  (x y : A) →
+  (k : ℕ) → is-π-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 =
+  λ 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-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-ℕ =
+  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
+    ( is-unbounded-π-finite-Id-is-unbounded-π-finite H x y)
+    ( k)
+```
+
+### Finite products of unbounded π-finite types are unbounded π-finite
+
+Agda is not convinced that the following proof is productive.
+
+```text
+is-unbounded-π-finite-Π :
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
+  is-finite A → ((a : A) → is-unbounded-π-finite (B a)) →
+  is-unbounded-π-finite ((a : A) → B a)
+is-unbounded-π-finite-Π H K =
+  λ where
+  .has-finitely-many-connected-components-is-unbounded-π-finite →
+    has-finitely-many-connected-components-finite-Π H
+      ( λ a →
+        has-finitely-many-connected-components-is-unbounded-π-finite (K a))
+  .is-unbounded-π-finite-Id-is-unbounded-π-finite f g →
+    is-unbounded-π-finite-equiv
+      ( equiv-funext)
+      ( is-unbounded-π-finite-Π H
+        ( λ a →
+          is-unbounded-π-finite-Id-is-unbounded-π-finite (K a) (f a) (g a)))
+```
+
+Instead, we give a proof using the description of unbounded π-finite types as
+types that are πₙ-finite for all n.
+
+```agda
+is-unbounded-π-finite-Π :
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
+  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
+    ( λ k →
+      is-π-finite-Π k H
+        ( λ a → is-π-finite-is-unbounded-π-finite (K a) k))
+```
+
+### Dependent sums of unbounded π-finite types are unbounded π-finite
+
+The dependent sum of a family of unbounded π-finite types over an unbounded
+π-finite base is unbounded π-finite.
+
+```agda
+abstract
+  is-unbounded-π-finite-Σ :
+    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
+    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
+      ( λ k →
+        is-π-finite-Σ k
+          ( is-π-finite-is-unbounded-π-finite H (succ-ℕ k))
+          ( λ x → is-π-finite-is-unbounded-π-finite (K x) k))
+```
+
+## References
+
+The category of unbounded π-finite spaces is considered in great detail in
+{{#cite Anel24}}.
+
+{{#bibliography}}
+
+## External links
+
+- [pi-finite type](https://ncatlab.org/nlab/show/pi-finite+type) at $n$Lab