Constructing categories and setoids of setoids in type theory

DOI10.2168/LMCS-10(3:25)2014zbMath1341.03012arXiv1408.1364MaRDI QIDQ2921123

Erik Palmgren, Olov Wilander

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

zbMATH Keywords

categoriesconstructive set theoryformalizationdependent type theorysetoids

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50)

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

• Coq
• MetaPRL

This page was built for publication: Constructing categories and setoids of setoids in type theory