Pages that link to "Item:Q2921123"
From MaRDI portal
The following pages link to Constructing categories and setoids of setoids in type theory (Q2921123):
Displaying 26 items.
- Relating first-order set theories, toposes and categories of classes (Q386623) (← links)
- Constructions of categories of setoids from proof-irrelevant families (Q512135) (← links)
- How to delete categorically -- two pushout complement constructions (Q631570) (← links)
- Proof-relevance of families of setoids and identity in type theory (Q661282) (← links)
- Categoricity results for second-order ZF in dependent type theory (Q1687749) (← links)
- Algebras of complemented subsets (Q2104273) (← links)
- Constructing a universe for the setoid model (Q2233391) (← links)
- Category theoretic structure of setoids (Q2253183) (← links)
- Categoricity results and large model constructions for second-order ZF in dependent type theory (Q2319994) (← links)
- Towards formalizing categorical models of type theory in type theory (Q2871881) (← links)
- Some proposals for the set-theoretic foundations of category theory (Q2926202) (← links)
- Idempotents in intensional type theory (Q2974780) (← links)
- (Q3527480) (← links)
- (Q3527490) (← links)
- (Q4370241) (← links)
- Heterogeneous Substitution Systems Revisited (Q4580223) (← links)
- Direct spectra of Bishop spaces and their limits (Q4989398) (← links)
- Proof-relevance in Bishop-style constructive mathematics (Q5055489) (← links)
- (Q5091143) (← links)
- EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS (Q5148098) (← links)
- W-types in setoids (Q5155691) (← links)
- Category Theory in Coq 8.5 (Q5369495) (← links)
- (Q5752573) (← links)
- From type theory to setoids and back (Q5889302) (← links)
- Sets completely separated by functions in Bishop set theory (Q6589312) (← links)
- Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory (Q6635512) (← links)
