The long exact sequence of homotopy $n$-groups

Ulrik Buchholtz, Egbert Rijke

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…