Homotopy automorphism groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2025-02-27.
Last modified on 2026-05-02.

module group-theory.homotopy-automorphism-groups where
Imports 
open import foundation.truncation-levels
open import foundation.truncations
open import foundation.universe-levels

open import group-theory.automorphism-groups
open import group-theory.concrete-groups

open import higher-group-theory.higher-groups

open import structured-types.pointed-types

Idea

The concrete homotopy automorphism group of a pointed type A is the automorphism group of the groupoidification of A at its base point.

Definitions

Homotopy automorphism groups of pointed types

module _
  {l : Level} (A : Pointed-Type l)
  where

  concrete-group-Pointed-Type : Concrete-Group l
  concrete-group-Pointed-Type =
    Automorphism-Group
      ( trunc one-𝕋 (type-Pointed-Type A))
      ( unit-trunc (point-Pointed-Type A))

  classifying-type-concrete-group-Pointed-Type : UU l
  classifying-type-concrete-group-Pointed-Type =
    classifying-type-Concrete-Group concrete-group-Pointed-Type

  shape-concrete-group-Pointed-Type :
    classifying-type-concrete-group-Pointed-Type
  shape-concrete-group-Pointed-Type =
    shape-Concrete-Group concrete-group-Pointed-Type

  ∞-group-concrete-group-Pointed-Type : ∞-Group l
  ∞-group-concrete-group-Pointed-Type =
    ∞-group-Concrete-Group concrete-group-Pointed-Type

Recent changes