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 that is n -exact at \| E\|ₙ₋₁ . 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.