The long exact sequence of homotopy $n$-groups

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 $\Vert F{\Vert }_{n-1}\to \Vert E{\Vert }_{n-1}\to \Vert B{\Vert }_{n-1}$ that is $n$-exact at $\Vert E{\Vert }_{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.

Updated version with improved exposition. Comments welcome