同伦 n-群的长正合序列

在同伦类型论中，我们引入带点类型的短序列 $F\to E\to B$ 的 $n$-正合性概念，并证明任意类型的纤维序列 $F\hookrightarrow E \twoheadrightarrow B$ 都诱导出一个在 $\|E\|_{n-1}$ 处 $n$-正合的短序列 $\|F\|_{n-1} \to \|E\|_{n-1} \to \|B\|_{n-1}$。我们解释了当用 $n$-群来解释时该指标设定的合理性，并将我们的定义与已有的 $n=1,2$ 时 $n$-群正合序列定义进行比较。作为主要应用，我们得到了纤维序列的同伦 $n$-群的长 $n$-正合序列。