Pages that link to "Item:Q1295396"
From MaRDI portal
The following pages link to Inaccessibility in constructive set theory and type theory (Q1295396):
Displaying 14 items.
- The constructive Hilbert program and the limits of Martin-Löf type theory (Q813417) (← links)
- Induction-recursion and initial algebras. (Q1412830) (← links)
- Inaccessible set axioms may have little consistency strength (Q1612481) (← links)
- Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe (Q1861330) (← links)
- Predicativity and constructive mathematics (Q2080590) (← links)
- Heyting-valued interpretations for constructive set theory (Q2575769) (← links)
- From Mathesis Universalis to Provability, Computability, and Constructivity (Q3305633) (← links)
- Realization of analysis into Explicit Mathematics (Q4328839) (← links)
- A general formulation of simultaneous inductive-recursive definitions in type theory (Q4508246) (← links)
- Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice (Q5060191) (← links)
- Proof Theory of Constructive Systems: Inductive Types and Univalence (Q5214792) (← links)
- A cumulative hierarchy of sets for constructive set theory (Q5404160) (← links)
- Dependent products and 1-inaccessible universes (Q5854448) (← links)
- From type theory to setoids and back (Q5889302) (← links)
