Higher group theory

Content created by Egbert Rijke, Fredrik Bakke and Victor Blanchi.

Created on 2023-04-10.
Last modified on 2025-02-27.

Modules in the higher group theory namespace

module higher-group-theory where

open import higher-group-theory.abelian-higher-groups public
open import higher-group-theory.automorphism-groups public
open import higher-group-theory.cartesian-products-higher-groups public
open import higher-group-theory.conjugation public
open import higher-group-theory.cyclic-higher-groups public
open import higher-group-theory.deloopable-groups public
open import higher-group-theory.deloopable-h-spaces public
open import higher-group-theory.deloopable-types public
open import higher-group-theory.eilenberg-mac-lane-spaces public
open import higher-group-theory.equivalences-higher-groups public
open import higher-group-theory.fixed-points-higher-group-actions public
open import higher-group-theory.free-higher-group-actions public
open import higher-group-theory.higher-group-actions public
open import higher-group-theory.higher-groups public
open import higher-group-theory.homomorphisms-higher-group-actions public
open import higher-group-theory.homomorphisms-higher-groups public
open import higher-group-theory.integers-higher-group public
open import higher-group-theory.iterated-cartesian-products-higher-groups public
open import higher-group-theory.iterated-deloopings-of-pointed-types public
open import higher-group-theory.orbits-higher-group-actions public
open import higher-group-theory.small-higher-groups public
open import higher-group-theory.subgroups-higher-groups public
open import higher-group-theory.symmetric-higher-groups public
open import higher-group-theory.transitive-higher-group-actions public
open import higher-group-theory.trivial-higher-groups public

Recent changes