Unbounded π-finite types (#1168)

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

@@ -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},

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

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>

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

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

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,13 +107,61 @@ 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
 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)