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



    Upload a copy of this work     Papers currently archived: 100,448

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.
Using Dependent Record Types in Clarification Ellipsis.Robin Cooper - unknown

Analytics

Added to PP
2014-01-16

Downloads
68 (#306,071)

6 months
13 (#242,872)

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.
Type Theory and Homotopy.Steve Awodey - 2012 - In Peter Dybjer, Sten Lindström, Erik Palmgren & Göran Sundholm (eds.), Epistemology Versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf. Dordrecht, Netherland: Springer. pp. 183-201.
Heyting-valued interpretations for Constructive Set Theory.Nicola Gambino - 2006 - Annals of Pure and Applied Logic 137 (1-3):164-188.
A brief introduction to algebraic set theory.Steve Awodey - 2008 - Bulletin of Symbolic Logic 14 (3):281-298.

View all 23 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