Connected components of types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Eléonore Mangel.

Created on 2022-02-16.
Last modified on 2023-11-24.

module foundation.connected-components where
Imports 
open import foundation.0-connected-types
open import foundation.dependent-pair-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.universe-levels

open import foundation-core.equality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.subtypes
open import foundation-core.truncated-types
open import foundation-core.truncation-levels

open import higher-group-theory.higher-groups

open import structured-types.pointed-types

Idea

The connected component of a type A at an element a : A is the type of all x : A that are merely equal to a.

The subtype of elements merely equal to a is also the least subtype of A containing a. In other words, if a subtype satisfies the universal property of being the least subtype of A containing a, then its underlying type is the connected component of A at a.

Definitions

The predicate of being the least subtype containing a given element

module _
  {l1 l2 : Level} {X : UU l1} (x : X) (P : subtype l2 X)
  where

  is-least-subtype-containing-element : UUω
  is-least-subtype-containing-element =
    {l : Level} (Q : subtype l X) → (P ⊆ Q) ↔ is-in-subtype Q x

Connected components of types

module _
  {l : Level} (A : UU l) (a : A)
  where

  connected-component : UU l
  connected-component =
    Σ A (λ x → type-trunc-Prop (x ＝ a))

  point-connected-component : connected-component
  pr1 point-connected-component = a
  pr2 point-connected-component = unit-trunc-Prop refl

  connected-component-Pointed-Type : Pointed-Type l
  pr1 connected-component-Pointed-Type = connected-component
  pr2 connected-component-Pointed-Type = point-connected-component

  value-connected-component :
    connected-component → A
  value-connected-component X = pr1 X

  abstract
    mere-equality-connected-component :
      (X : connected-component) →
      type-trunc-Prop (value-connected-component X ＝ a)
    mere-equality-connected-component X = pr2 X

Properties

Connected components are 0-connected

abstract
  is-0-connected-connected-component :
    {l : Level} (A : UU l) (a : A) →
    is-0-connected (connected-component A a)
  is-0-connected-connected-component A a =
    is-0-connected-mere-eq
      ( a , unit-trunc-Prop refl)
      ( λ (x , p) →
        apply-universal-property-trunc-Prop
          ( p)
          ( trunc-Prop ((a , unit-trunc-Prop refl) ＝ (x , p)))
          ( λ p' →
            unit-trunc-Prop
              ( eq-pair-Σ
                ( inv p')
                ( all-elements-equal-type-trunc-Prop _ p))))

connected-component-∞-Group :
  {l : Level} (A : UU l) (a : A) → ∞-Group l
pr1 (connected-component-∞-Group A a) = connected-component-Pointed-Type A a
pr2 (connected-component-∞-Group A a) = is-0-connected-connected-component A a

If A is k+1-truncated, then the connected component of a in A is k+1-truncated

is-trunc-connected-component :
  {l : Level} {k : 𝕋} (A : UU l) (a : A) →
  is-trunc (succ-𝕋 k) A → is-trunc (succ-𝕋 k) (connected-component A a)
is-trunc-connected-component {l} {k} A a H =
  is-trunc-Σ H (λ x → is-trunc-is-prop k is-prop-type-trunc-Prop)

Recent changes