Wellfounded trees in categories
From MaRDI portal
Publication:1577483
DOI10.1016/S0168-0072(00)00012-9zbMath1010.03056WikidataQ126323888 ScholiaQ126323888MaRDI QIDQ1577483
Publication date: 8 May 2003
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Functional programming and lambda calculus (68N18) Categorical logic, topoi (03G30) Topoi (18B25) Categorical semantics of formal languages (18C50) Second- and higher-order arithmetic and fragments (03F35) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Foundations, relations to logic and deductive systems (18A15)
Related Items
Data Types with Symmetries and Polynomial Functors over Groupoids, Well-foundedness in realizability, Non-well-founded trees in categories, Relating first-order set theories, toposes and categories of classes, On the dependent product in toposes, Non-deterministic inductive definitions, Universal properties of bicategories of polynomials, A class of higher inductive types in Zermelo‐Fraenkel set theory, The compatibility of the minimalist foundation with homotopy type theory, Unnamed Item, Derived rules for predicative set theory: an application of sheaves, Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets, Constructive toposes with countable sums as models of constructive set theory, Polynomial functors and combinatorial Dyson–Schwinger equations, Unnamed Item, Unnamed Item, Cacti and filtered distributive laws, EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS, Polynomial functors and polynomial monads, Partiality, State and Dependent Types, Algebraic set theory and the effective topos, Local fibred right adjoints are polynomial, The associated sheaf functor theorem in algebraic set theory, Aspects of predicative algebraic set theory. I: Exact completion, Unnamed Item, Monads in double categories, W-types in homotopy type theory, Inductive types and exact completion, Combining effects: sum and tensor, Unnamed Item, Unnamed Item, Type theories, toposes and constructive set theory: Predicative aspects of AST, The simplicial model of univalent foundations (after Voevodsky), A Brief Introduction to Algebraic Set Theory, Three extensional models of type theory, The generalised type-theoretic interpretation of constructive set theory, W-types in setoids, A minimalist two-level foundation for constructive mathematics, Unnamed Item, The universal exponentiable arrow, Wellfounded trees in categories, Models of Type Theory Based on Moore Paths, Containers: Constructing strictly positive types, Homotopy theory for algebras over polynomial monads, Type Theory and Homotopy, Heyting-valued interpretations for constructive set theory, The axiom of multiple choice and models for constructive set 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
