We develop a uniform type theory that integrates intensionality, extensionality and proof irrelevance as judgmental concepts. Any object may be treated intensionally (subject only to /spl alpha/-conversion), extensionally (subject also to /spl beta//spl eta/-conversion), or as irrelevant (equal to any other object at the same type), depending on where it occurs. Modal restrictions developed by R. Harper et al. (2000) for single types are generalized and employed to guarantee consistency between these views of objects. Potential applications are in logical frameworks, functional programming and the foundations of first-order modal logics. Our type theory contrasts with previous approaches that, a priori, distinguished propositions (whose proofs are all identified - only their existence is important) from specifications (whose implementations are subject to some definitional equalities).
展开▼
机译：我们开发了一种统一类型理论，将意图性，可扩展性和证明无关紧要作为判断概念进行了整合。任何对象都可以被故意（仅受/ spl alpha / -conversion约束），扩展（也受/ spl beta // spl eta / -conversion约束）或无关紧要（等同于同一类型的任何其他对象）对待，取决于它发生的位置。 R. Harper等人开发的模态限制。 （2000）对单个类型进行了概括，并采用它们来保证这些对象视图之间的一致性。潜在的应用是在逻辑框架，功能编程和一阶模态逻辑的基础中。我们的类型理论与先前的方法形成对比，即先验的，与规范（其实现受某些定义的平等性约束）不同的命题（所有证据都被确定-仅它们的存在很重要）。
展开▼
