This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Higher group theory

Files in the higher group theory folder

module higher-group-theory where

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