Non-deterministic inductive definitions
From MaRDI portal
Publication:1935375
DOI10.1007/s00153-012-0309-4zbMath1403.03111arXiv1104.2744MaRDI QIDQ1935375
Publication date: 15 February 2013
Published in: Archive for Mathematical Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1104.2744
type theory; constructive set theory; formal topology; predicativity; inductive and coinductive types
Related Items
ELIMINATING DISJUNCTIONS BY DISJUNCTION ELIMINATION, Generalized geometric theories and set-generated classes, Eliminating disjunctions by disjunction elimination, Equivalents of the finitary non-deterministic inductive definitions
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Derived rules for predicative set theory: an application of sheaves
- Non-well-founded trees in categories
- The strength of some Martin-Löf type theories
- Some points in formal topology.
- Wellfounded trees in categories
- Constructive completions of ordered sets, groups and fields
- Characterizing the interpretation of set theory in Martin-Löf type theory
- Aspects of general topology in constructive set theory
- Maximal and partial points in formal spaces
- The axiom of multiple choice and models for constructive set theory
- Real and Ideal in Constructive Mathematics
- Generalized geometric theories and set-generated classes
- Completeness and cocompleteness of the categories of basic pairs and concrete spaces