Finiteness of the type of connected components

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

Created on 2022-02-17.
Last modified on 2023-03-13.

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)

Recent changes