Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unbounded π-finite types #1168

Open
wants to merge 14 commits into
base: master
Choose a base branch
from
10 changes: 10 additions & 0 deletions references.bib
Original file line number Diff line number Diff line change
Expand Up @@ -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},
Expand Down
10 changes: 10 additions & 0 deletions src/foundation/functoriality-set-truncation.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion src/polytopes/abstract-polytopes.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ open import elementary-number-theory
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
Expand All @@ -24,7 +25,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>
Expand Down
6 changes: 6 additions & 0 deletions src/univalent-combinatorics.lagda.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,9 @@
# Univalent combinatorics

```agda
{-# OPTIONS --guardedness #-}
```

## Idea

Univalent combinatorics is the study of finite univalent mathematics. Finiteness
Expand Down Expand Up @@ -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
Expand Down
9 changes: 6 additions & 3 deletions src/univalent-combinatorics/equality-finite-types.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
```

Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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)
Loading
Loading