The long exact sequence of homotopy n-groups

Working in homotopy type theory, we introduce the notion of n-exactness for a short sequence F -> E -> B of pointed types and show that any fiber sequence F -> E -> B of arbitrary types induces a short sequence||F||(n-1) -> ||E||(n-1) -> ||B||(n-1)that is n-exact at ||E||(n-1). We explain how the indexing makes sense when interpreted in terms of n-groups, and we compare our definition to the existing definitions of an exact sequence of n-groups for n = 1, 2. As the main application, we obtain the long n-exact sequence of homotopy n-groups of a fiber sequence.

Automated summary

Working in homotopy type theory, this paper introduces the notion of n-exactness for short sequences and explores the n-group properties of fiber sequences.