Category theoretic structure of setoids
DOI10.1016/j.tcs.2014.03.006zbMath1418.18006OpenAlexW2118319342MaRDI QIDQ2253183
Yoshiki Kinoshita, A. John Power
Publication date: 25 July 2014
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2014.03.006
coproductCartesian closed categoryproof assistantsetoidproof irrelevance\(\mathcal E\)-category\(\mathcal E\)-coinserterEquiv-categoryEquiv-inserter
Nonclassical and second-order set theories (03E70) Categories admitting limits (complete categories), functors preserving limits, completions (18A35) Enriched categories (over closed or monoidal categories) (18D20) Categories of sets, characterizations (18B05)
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Locally cartesian closed exact completions
- Some free constructions in realizability and proof theory
- Constructing a small category of setoids
- Setoids and universes
- Elementary observations on 2-categorical limits
- Normalization and the Yoneda embedding
- Introduction to bicategories
This page was built for publication: Category theoretic structure of setoids