Wellfounded Trees and Dependent Polynomial Functors
Wellfounded Trees and Dependent Polynomial Functors
复制标题
有根树和相关多项式函子
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
M. Hyland
中科院分区：
文献类型：
--
作者：
N. Gambino;M. Hyland
我们着手研究依赖类型理论中有充分根据的树类型假设的后果。我们通过研究[16]中引入的有根据的树的分类概念来做到这一点。我们的主要结果表明，有根据的树允许我们为局部笛卡尔闭类别上的广泛的内函子定义初始代数。
We set out to study the consequences of the assumption of types of wellfounded trees in dependent type theories. We do so by investigating the categorical notion of wellfounded tree introduced in [16]. Our main result shows that wellfounded trees allow us to define initial algebras for a wide class of endofunctors on locally cartesian closed categories.