Projects per year
Abstract
A setoid is a set together with a constructive representation of an equivalence relation on it. Here, we give category theoretic support to the notion. We first define a category Setoid and prove it is cartesian closed with coproducts. We then enrich it in the cartesian closed category Equiv of sets and classical equivalence relations, extend the above results, and prove that Setoid as an Equivenriched category has a relaxed form of equalisers. We then recall the definition of Ecategory, generalising that of Equivenriched category, and show that Setoid as an Ecategory has a relaxed form of coequalisers. In doing all this, we carefully compare our category theoretic constructs with Agda code for typetheoretic constructs on setoids.
Original language  English 

Pages (fromto)  145163 
Journal  Theoretical Computer Science 
Volume  546 
DOIs  
Publication status  Published  Aug 2014 
Keywords
 setoid
 proof assistant
 proof irrelevance
 Cartesian closed category
 coproduct
 Equivcategory
 Equivinserter
 Ecategory
 Ecoinserter
Fingerprint Dive into the research topics of 'Category theoretic structure of setoids'. Together they form a unique fingerprint.
Projects
 1 Finished

Coalgebraic Logic Programming for Type Inference
Power, J.
Engineering and Physical Sciences Research Council
1/09/13 → 31/01/17
Project: Research council