Constructing categories and setoids of setoids in type theory
From MaRDI portal
Publication:2921123
DOI10.2168/LMCS-10(3:25)2014zbMath1341.03012arXiv1408.1364MaRDI QIDQ2921123
Publication date: 30 September 2014
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1408.1364
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (10)
From type theory to setoids and back ⋮ Proof-relevance in Bishop-style constructive mathematics ⋮ Direct spectra of Bishop spaces and their limits ⋮ EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS ⋮ Constructing a universe for the setoid model ⋮ Constructions of categories of setoids from proof-irrelevant families ⋮ Unnamed Item ⋮ W-types in setoids ⋮ Heterogeneous Substitution Systems Revisited ⋮ Algebras of complemented subsets
Uses Software
This page was built for publication: Constructing categories and setoids of setoids in type theory
