Wellfounded trees in categories

&
Annals of Pure and Applied Logic 104 (1-3):189-218 (2000)
  Copy   BIBTEX

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

Categories

Keywords

Reprint years

DOI

10.1016/s0168-0072(00)00012-9

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 104,641

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Non-well-founded trees in categories.Benno van den Berg & Federico De Marchi - 2007 - Annals of Pure and Applied Logic 146 (1):40-59.
Modules in the category of sheaves over quantales.Marcelo E. Coniglio & Francisco Miraglia - 2001 - Annals of Pure and Applied Logic 108 (1-3):103-136.
Martin-Löf complexes.S. Awodey & M. A. Warren - 2013 - Annals of Pure and Applied Logic 164 (10):928-956.
Analytic ideals and cofinal types.Alain Louveau & Boban Velickovi - 1999 - Annals of Pure and Applied Logic 99 (1-3):171-195.
Recursive unary algebras and trees.Bakhadyr Khoussainov - 1994 - Annals of Pure and Applied Logic 67 (1-3):213-268.
Generalising canonical extension to the categorical setting.Dion Coumans - 2012 - Annals of Pure and Applied Logic 163 (12):1940-1961.
Categorical and algebraic aspects of Martin-löf type theory.Adam Obtułowicz - 1989 - Studia Logica 48 (3):299 - 317.
Algebraically closed MV-algebras and their sheaf representation.Antonio Di Nola, Anna R. Ferraioli & Giacomo Lenzi - 2013 - Annals of Pure and Applied Logic 164 (3):349-355.
Finite covers with finite kernels.David M. Evans - 1997 - Annals of Pure and Applied Logic 88 (2-3):109-147.
Well-ordering proofs for Martin-Löf type theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.

Analytics

Added to PP
2014-01-16

Downloads
82 (#273,073)

6 months
18 (#168,793)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

A minimalist two-level foundation for constructive mathematics.Maria Emilia Maietti - 2009 - Annals of Pure and Applied Logic 160 (3):319-354.
Heyting-valued interpretations for Constructive Set Theory.Nicola Gambino - 2006 - Annals of Pure and Applied Logic 137 (1-3):164-188.
Type Theory and Homotopy.Steve Awodey - 2012 - In Peter Dybjer, Sten Lindström, Erik Palmgren & Göran Sundholm, Epistemology Versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf. Dordrecht, Netherland: Springer. pp. 183-201.
A brief introduction to algebraic set theory.Steve Awodey - 2008 - Bulletin of Symbolic Logic 14 (3):281-298.

View all 25 citations / Add more citations

References found in this work

Forcing in intuitionistic systems without power-set.R. J. Grayson - 1983 - Journal of Symbolic Logic 48 (3):670-682.
Intuitionistic choice and classical logic.Thierry Coquand & Erik Palmgren - 2000 - Archive for Mathematical Logic 39 (1):53-74.

Add more references