scientific article
From MaRDI portal
Publication:3937387
zbMath0481.03035MaRDI QIDQ3937387
Publication date: 1978
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
dependent choicesrestricted excluded middlefull separationpowerset axiomMartin-Loef's intuitionistic theory of typespresentation axiomtype of sets
Related Items
THE AXIOM OF CHOICE IS FALSE INTUITIONISTICALLY (IN MOST CONTEXTS), From type theory to setoids and back, Computational adequacy for recursive types in models of intuitionistic set theory, The strength of some Martin-Löf type theories, Are there enough injective sets?, Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice, CZF does not have the existence property, Binary refinement implies discrete exponentiation, The semantics of realizability for the constructive set theory based on hyperarithmetical predicates, On generalized algebraic theories and categories with families, THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY, Non-well-founded trees in categories, Exact approximations to Stone-Čech compactification, Relating first-order set theories, toposes and categories of classes, Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language, On the local Cartesian closure of exact completions, Higher-order games with dependent types, A Comparison of Type Theory with Set Theory, Topological forcing semantics with settling, EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY, Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory, Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version, Distributive laws for relative monads, Unnamed Item, Towards a constructive simplicial model of Univalent Foundations, C-system of a module over a \(Jf\)-relative monad, On the \(T_{1}\) axiom and other separation properties in constructive point-free and point-set topology, 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, Constructive metrisability in point-free topology., Representing model theory in a type-theoretical logical framework, Proof-relevance of families of setoids and identity in type theory, EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS, Constructing a universe for the setoid model, A CONSTRUCTIVE EXAMINATION OF A RUSSELL-STYLE RAMIFIED TYPE THEORY, On Feferman's operational set theory \textsf{OST}, From Mathesis Universalis to Provability, Computability, and Constructivity, The weak choice principle WISC may fail in the category of sets, Extending constructive operational set theory by impredicative principles, A cumulative hierarchy of sets for constructive set theory, The Zariski spectrum as a formal geometry, Homotopy type-theoretic interpretations of constructive set theories, Exact completion of path categories and algebraic set theory. I: Exact completion of path categories, Aspects of predicative algebraic set theory. I: Exact completion, The paradox of trees in type theory, Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice, Aspects of predicative algebraic set theory. II: Realizability, Kronecker's density theorem and irrational numbers in constructive reverse mathematics, Independence results around constructive ZF, Kripke models for subtheories of \textsf{CZF}, Quotient topologies in constructive set theory and type theory, Characterizing the interpretation of set theory in Martin-Löf type theory, Unnamed Item, On the constructive Dedekind reals, Multisets in type theory, CONSTRUCTIVE REFLECTIVITY PRINCIPLES FOR REGULAR THEORIES, The strength of extensionality. I: Weak weak set theories with infinity, A meaning explanation for HoTT, Full operational set theory with unbounded existential quantification and power set, Categoricity results and large model constructions for second-order ZF in dependent type theory, Predicativity and constructive mathematics, Problems, solutions, and completions, Replacement versus collection and related topics in constructive Zermelo-Fraenkel set theory, Gödel and Intuitionism, Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions, On the collection of points of a formal space, Heyting-valued interpretations for constructive set theory, A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\), On the compatibility between the minimalist foundation and constructive set theory, Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe, Syntax for Semantics: Krull’s Maximal Ideal Theorem
