Wellfounded trees in categories

被引：74

作者：

Moerdijk, I

Palmgren, E

机构：

[1] Uppsala Univ, Matemat Inst, S-75106 Uppsala, Sweden

[2] Univ Utrecht, Math Inst, NL-3508 TA Utrecht, Netherlands

来源：

ANNALS OF PURE AND APPLIED LOGIC | 2000年 / 104卷 / 1-3期

基金：

瑞典研究理事会;

关键词：

initial algebras; locally cartesian closed categories; pretoposes; Artin gluing; sheaves; wellfounded trees; Martin-Lof type theory;

D O I：

10.1016/S0168-0072(00)00012-9

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

In this paper we present and study a categorical formulation of the W-types of Martin-Lof. These are essentially free term algebras where the operations may have finite or infinite arity. It is shown that W-types are preserved under the construction of sheaves and Artin gluing. In the proofs we avoid using impredicative or nonconstructive principles. (C) 2000 Elsevier Science B.V. All rights reserved. MSG: primary: 03B15; 03G30; 18A15; 18B25; 18C15; 18F20; secondary: 18C50; 68N18.

引用

页码：189 / 218

页数：30

共 20 条

[1] FIBERED CATEGORIES AND THE FOUNDATIONS OF NAIVE CATEGORY THEORY [J].