Category theoretic structure of setoids


Kinoshita, Y. and Power, J., 2014. Category theoretic structure of setoids. Theoretical Computer Science, 546, pp. 145-163.

Related documents:

PDF (Category Theoretic Structure of Setoids (pdf)) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (397kB) | Preview

    Official URL:


    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.


    Item Type Articles
    CreatorsKinoshita, Y.and Power, J.
    Uncontrolled Keywordssetoid,proof assistant,proof irrelevance,cartesian closed category,coproduct,equiv-category,equiv-inserter,e-category,e-coinserter
    DepartmentsFaculty of Science > Computer Science
    Publisher Statementmain.pdf: NOTICE: this is the author’s version of a work that was accepted for publication in Theoretical Computer Science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version will be published in Theoretical Computer Science
    ID Code34231


    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...