# Trivial concrete groups

Content created by Fredrik Bakke.

Created on 2023-09-15.

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

open import group-theory.concrete-groups

open import higher-group-theory.trivial-higher-groups

## Idea

A concrete group G is trivial if its classifying type is contractible.

## Definitions

### Trivial higher groups

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

is-trivial-prop-Concrete-Group : Prop l
is-trivial-prop-Concrete-Group =
is-trivial-prop-∞-Group (∞-group-Concrete-Group G)

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

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

### Higher groups with contractible classifying type

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

has-contractible-classifying-type-prop-Concrete-Group : Prop l
has-contractible-classifying-type-prop-Concrete-Group =
has-contractible-classifying-type-prop-∞-Group (∞-group-Concrete-Group G)

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

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

### The trivial concrete group

trivial-Concrete-Group : {l : Level}  Concrete-Group l
pr1 trivial-Concrete-Group = trivial-∞-Group
pr2 trivial-Concrete-Group =
is-trunc-is-contr (one-𝕋) (is-contr-raise-unit) (raise-star) (raise-star)

has-contractible-classifying-type-trivial-Concrete-Group :
{l : Level}
has-contractible-classifying-type-Concrete-Group (trivial-Concrete-Group {l})
has-contractible-classifying-type-trivial-Concrete-Group =
has-contractible-classifying-type-trivial-∞-Group

## Properties

### Having contractible classifying type is equivalent to having contractible underlying type

This remains to be formalized.