# Trivial higher groups

Content created by Fredrik Bakke.

Created 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.