Wellfounded trees in categories

DOI10.1016/S0168-0072(00)00012-9zbMath1010.03056MaRDI QIDQ1577483

Ieke Moerdijk, Erik Palmgren

Publication date: 8 May 2003

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

sheaves; Artin gluing; free term algebras; W-types

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

03G30: Categorical logic, topoi

18B25: Topoi

18C50: Categorical semantics of formal languages

03F35: Second- and higher-order arithmetic and fragments

18C15: Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads

18F20: Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects)

18A15: Foundations, relations to logic and deductive systems

Related Items

The generalised type-theoretic interpretation of constructive set theory, Algebraic set theory and the effective topos, Type theories, toposes and constructive set theory: Predicative aspects of AST, Inductive types and exact completion, Well-foundedness in realizability, Non-well-founded trees in categories, The associated sheaf functor theorem in algebraic set theory, Aspects of predicative algebraic set theory. I: Exact completion, A minimalist two-level foundation for constructive mathematics, Wellfounded trees in categories, Combining effects: sum and tensor, Containers: Constructing strictly positive types, Heyting-valued interpretations for constructive set theory, A Brief Introduction to Algebraic Set Theory, Three extensional models of type theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Sheaves in geometry and logic: a first introduction to topos theory
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Wellfounded trees in categories
• Artin glueing
• Intuitionistic choice and classical logic
• A fixpoint theorem for complete categories
• Locally cartesian closed categories and type theory
• Fibered categories and the foundations of naive category theory
• Forcing in intuitionistic systems without power-set
• Extensional Constructs in Intensional Type Theory
• Type theories, toposes and constructive set theory: Predicative aspects of AST