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 Equiv-enriched category has a relaxed form of equalisers. We then recall the definition of E-category, generalising that of Equiv-enriched category, and show that Setoid as an E-category has a relaxed form of coequalisers. In doing all this, we carefully compare our category theoretic constructs with Agda code for type-theoretic constructs on setoids.

Original language | English |
---|---|

Pages (from-to) | 145-163 |

Journal | Theoretical Computer Science |

Volume | 546 |

DOIs | |

Publication status | Published - Aug 2014 |

### Keywords

- setoid
- proof assistant
- proof irrelevance
- Cartesian closed category
- coproduct
- Equiv-category
- Equiv-inserter
- E-category
- E-coinserter

## 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

## Cite this

Kinoshita, Y., & Power, J. (2014). Category theoretic structure of setoids.

*Theoretical Computer Science*,*546*, 145-163. https://doi.org/10.1016/j.tcs.2014.03.006