Wellfounded trees in categories
From MaRDI portal
Second- and higher-order arithmetic and fragments (03F35) Categorical logic, topoi (03G30) Foundations, relations to logic and deductive systems (18A15) Topoi (18B25) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Categorical semantics of formal languages (18C50) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Functional programming and lambda calculus (68N18)
Recommendations
Cites work
- A fixpoint theorem for complete categories
- Artin glueing
- Extensional constructs in intensional type theory
- Fibered categories and the foundations of naive category theory
- Forcing in intuitionistic systems without power-set
- scientific article; zbMATH DE number 445156 (Why is no real title available?)
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 45228 (Why is no real title available?)
- scientific article; zbMATH DE number 3574077 (Why is no real title available?)
- scientific article; zbMATH DE number 2079044 (Why is no real title available?)
- Intuitionistic choice and classical logic
- Locally cartesian closed categories and type theory
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory
- Sheaves in geometry and logic: a first introduction to topos theory
- Type theories, toposes and constructive set theory: Predicative aspects of AST
- Wellfounded trees in categories
Cited in
(57)- A minimalist two-level foundation for constructive mathematics
- Wellfounded trees in categories
- Non-deterministic inductive definitions
- The simplicial model of univalent foundations (after Voevodsky)
- The universal exponentiable arrow
- Universal properties of bicategories of polynomials
- Combining effects: sum and tensor
- Containers: Constructing strictly positive types
- Heyting-valued interpretations for constructive set theory
- The axiom of multiple choice and models for constructive set theory
- Homotopy theory for algebras over polynomial monads
- Polynomial functors and combinatorial Dyson-Schwinger equations
- Partiality, state and dependent types
- scientific article; zbMATH DE number 7037626 (Why is no real title available?)
- Data types with symmetries and polynomial functors over groupoids
- A Brief Introduction to Algebraic Set Theory
- Three extensional models of type theory
- Relating first-order set theories, toposes and categories of classes
- 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
- Models of type theory based on Moore paths
- Cacti and filtered distributive laws
- Polynomial functors and polynomial monads
- Local fibred right adjoints are polynomial
- Dependent inductive and coinductive types are fibrational dialgebras
- Cubical syntax for reflection-free extensional equality
- Quotients, inductive types, and quotient inductive types
- Models of Type Theory Based on Moore Paths
- Exact completion and constructive theories of sets
- W-types in setoids
- Type theory and homotopy
- Monads in double categories
- Automata, Languages and Programming
- scientific article; zbMATH DE number 5023079 (Why is no real title available?)
- The generalised type-theoretic interpretation of constructive set theory
- Inductive types and exact completion
- Algebraic set theory and the effective topos
- W-types in homotopy type theory
- Type theories, toposes and constructive set theory: Predicative aspects of AST
- On the dependent product in toposes
- A class of higher inductive types in Zermelo‐Fraenkel set theory
- The compatibility of the minimalist foundation with homotopy type theory
- Constructing initial algebras using inflationary iteration
- Native type theory
- Computads for weak -categories as an inductive type
- Automata in W-toposes, and general Myhill-Nerode theorems
- Classifying topoi in synthetic guarded domain theory
- On the existence and disjunction properties in structural set theory
- A topological reading of coinductive predicates in dependent type theory
- Comodule representations of second-order functionals
- Broad infinity and generation principles
- Functoriality of enriched data types
- 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
This page was built for publication: Wellfounded trees in categories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1577483)
