The long exact sequence of homotopy $n$-groups

TL;DR

This paper develops a notion of $n$-exactness in homotopy type theory, establishing a long exact sequence of homotopy $n$-groups for fiber sequences, extending classical concepts to higher homotopy levels.

Contribution

It introduces the concept of $n$-exactness for sequences of pointed types and constructs a long $n$-exact sequence of homotopy $n$-groups within homotopy type theory.

Findings

Defined $n$-exactness for sequences of pointed types.

Proved that fiber sequences induce $n$-exact sequences of homotopy $n$-groups.

Compared new definitions with existing ones for $n=1,2$.

Abstract

Working in homotopy type theory, we introduce the notion of $n$-exactness for a short sequence $F\to E\to B$ of pointed types, and show that any fiber sequence $F\hookrightarrow E \twoheadrightarrow B$ of arbitrary types induces a short sequence $\|F\|_{n-1} \to \|E\|_{n-1} \to \|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.