# Finiteness of the type of connected components

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-02-17.

module univalent-combinatorics.finite-connected-components where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.propositions
open import foundation.set-truncations
open import foundation.universe-levels

open import univalent-combinatorics.finite-types


## Idea

A type is said to have finitely many connected components if its set truncation is a finite type.

## Definition

has-finitely-many-components-Prop : {l : Level} → UU l → Prop l
has-finitely-many-components-Prop A = is-finite-Prop (type-trunc-Set A)

has-finitely-many-components : {l : Level} → UU l → UU l
has-finitely-many-components A = type-Prop (has-finitely-many-components-Prop A)

has-cardinality-components-Prop : {l : Level} (k : ℕ) → UU l → Prop l
has-cardinality-components-Prop k A =
has-cardinality-Prop k (type-trunc-Set A)

has-cardinality-components : {l : Level} (k : ℕ) → UU l → UU l
has-cardinality-components k A =
type-Prop (has-cardinality-components-Prop k A)