In Feferman's work, explicit mathematics and theories of generalized inductive definitions play a central role. One objective of this article is to describe the connections with Martin-Lof type theory and constructive Zermelo-Fraenkel set theory. Proof theory has contributed to a deeper grasp of the relationship between different frameworks for constructive mathematics. Some of the reductions are known only through ordinal-theoretic characterizations. The paper also addresses the strength of Voevodsky's univalence axiom. A further goal is to investigate the strength of intuitionistic theories of generalized inductive definitions in the framework of intuitionistic explicit mathematics that lie beyond the reach of Martin-Lof type theory.
众所周知，univalence与unique of identity proofs（UIP）是不相容的，UIP是所有类型都是h-集的公理。这是由于有限的h-集只要不是h-命题就有非平凡的自同构。一个自然的问题是，限制于h-命题的单价是否与UIP相容。我们通过构建一个模型来肯定地回答这个问题，在这个模型中，类型是同伦类型论中定义为更高归纳类型的封闭宇宙的元素。这个宇宙有一个同时“部分”单价完成的路径构造器，即，仅限于H命题。更一般地说，我们表明，单价限于$(n-1)$类型是一致的假设，所有类型的$n$截断。此外，我们参数化我们的建设一个适当的良好的行为容器，抽象从一个具体的选择类型的former的宇宙。
Equivalents of the finitary non-deterministic inductive definitions
我们给出了等价于van den Berg（2013）的非确定性归纳定义（NID）原理的一些片段的陈述，该原理在构造性集合论CZF的弱子系统中工作。我们表明，在建设性的拓扑结构，最初证明了使用NID的几个语句是等价的初等和有限NID。我们还表明，有限NID是等价于它的二进制片段和初等NID是等价于NID的双闭子集的概念的基础上的一个变种。我们的结果表明，证明这些陈述的建设性拓扑需要真正的扩展CZF的基本或有限NID。
同伦类型论（英语：Homotopy type theory）是马丁-勒夫的构造性类型论在抽象同伦理论中的一种解释。有结果之间的联系建设性数学和代数拓扑，提供拓扑语义内涵系统的类型理论，以及计算方法，代数拓扑通过类型理论为基础的证明助手，如Coq。目前的工作调查归纳类型在这种情况下。修改规则的归纳类型，包括类型的良基树，或W型，提出了，并确定了基本的同伦语义，这样的类型。所有结果的证明都已由Coq证明助理正式验证，并且用于此验证的证明脚本构成了本研究的重要组成部分。
