The Long Exact Sequence of Higher Groups

An n-group in homotopy type theory is simply defined to be a pointed connected n-type. With this definition, an ordinary 1-group is a pointed connected 1-type. In other words, a 1-group is presented as its classifying space, and we think of higher groups as presented in that way too. The fundamental n-group of a type X at x is then simply the n-truncation of the connected component of X. We formulate a notion of n-exactness, and show that any fiber sequence F -> E -> B of pointed types induces a long n-exact sequence of homotopy n-groups.