Title of article
Wellfounded trees in categories Original Research Article
Author/Authors
Ieke Moerdijk، نويسنده , , Erik Palmgren، نويسنده ,
Issue Information
روزنامه با شماره پیاپی سال 2000
Pages
30
From page
189
To page
218
Abstract
In this paper we present and study a categorical formulation of the W-types of Martin-Löf. 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.
Keywords
Initial algebras , Pretoposes , Artin gluing , Sheaves , Wellfounded trees , Martin-L?f type theory , Locally cartesian closed categories
Journal title
Annals of Pure and Applied Logic
Serial Year
2000
Journal title
Annals of Pure and Applied Logic
Record number
889730
Link To Document