直觉主义类型论中π和Σ规则的研究

On the π and Σ rules in intuitionistic type theory

本文研究直觉主义类型论中π和Σ规则，对于类型（πｘ∈Ａ）Ｂ（ｘ），我们给出新的消去和相等规则使新规则的式样与其他类型的规则相同，然而不使用高阶交元和常元，我们证明新规则等价于旧规则，对于类型（Σｘ∈Ａ）Ｂ（ｘ），我们利用投影运算给出新规则，而且证明它们等价于旧规则。

This paper is devoted to the π and Σ-rules in the intuitionistic type theory. For the type (πx∈A)B(x), we formulate new elimination and equality rules,which have the same pattern as the other type rules, but the higher level variable and constants are not used. We prove that the new rules are equivalent to the old ones. For the type (Σx∈A )B(x), we also formulate new elimination and equality rules by means of the projetions. the new rules are proved to the equivalent to the old ones.