Trivial higher groups

Content created by Fredrik Bakke.

Created on 2023-09-15.
Last modified on 2023-09-15.

module higher-group-theory.trivial-higher-groups where
Imports 
open import foundation.0-connected-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.unit-type
open import foundation.universe-levels

open import higher-group-theory.higher-groups

Idea

A higher group G is trivial if its underlying type is contractible.

Definitions

Trivial higher groups

module _
  {l : Level} (G : ∞-Group l)
  where

  is-trivial-prop-∞-Group : Prop l
  is-trivial-prop-∞-Group = is-contr-Prop (type-∞-Group G)

  is-trivial-∞-Group : UU l
  is-trivial-∞-Group = type-Prop is-trivial-prop-∞-Group

  is-property-is-trivial-∞-Group : is-prop (is-trivial-∞-Group)
  is-property-is-trivial-∞-Group = is-prop-type-Prop is-trivial-prop-∞-Group

Higher groups with contractible classifying type

module _
  {l : Level} (G : ∞-Group l)
  where

  has-contractible-classifying-type-prop-∞-Group : Prop l
  has-contractible-classifying-type-prop-∞-Group =
    is-contr-Prop (classifying-type-∞-Group G)

  has-contractible-classifying-type-∞-Group : UU l
  has-contractible-classifying-type-∞-Group =
    type-Prop has-contractible-classifying-type-prop-∞-Group

  is-property-has-contractible-classifying-type-∞-Group :
    is-prop (has-contractible-classifying-type-∞-Group)
  is-property-has-contractible-classifying-type-∞-Group =
    is-prop-type-Prop has-contractible-classifying-type-prop-∞-Group

The trivial higher group

trivial-∞-Group : {l : Level} → ∞-Group l
pr1 (pr1 (trivial-∞-Group {l})) = raise-unit l
pr2 (pr1 trivial-∞-Group) = raise-star
pr2 (trivial-∞-Group {l}) =
  is-0-connected-is-contr (raise-unit l) is-contr-raise-unit

has-contractible-classifying-type-trivial-∞-Group :
  {l : Level} → has-contractible-classifying-type-∞-Group (trivial-∞-Group {l})
has-contractible-classifying-type-trivial-∞-Group = is-contr-raise-unit

Properties

Having contractible classifying type is equivalent to having contractible underlying type

This remains to be formalized.

Recent changes