Erik Palmgren ; Olov Wilander - Constructing categories and setoids of setoids in type theory

lmcs:964 - Logical Methods in Computer Science, September 23, 2014, Volume 10, Issue 3 - https://doi.org/10.2168/LMCS-10(3:25)2014
Constructing categories and setoids of setoids in type theoryArticle

Authors: Erik Palmgren ; Olov Wilander

    In this paper we consider the problem of building rich categories of setoids, in standard intensional Martin-Löf type theory (MLTT), and in particular how to handle the problem of equality on objects in this context. Any (proof-irrelevant) family F of setoids over a setoid A gives rise to a category C(A, F) of setoids with objects A. We may regard the family F as a setoid of setoids, and a crucial issue in this article is to construct rich or large enough such families. Depending on closure conditions of F, the category C(A, F) has corresponding categorical constructions. We exemplify this with finite limits. A very large family F may be obtained from Aczel's model construction of CZF in type theory. It is proved that the category so obtained is isomorphic to the internal category of sets in this model. Set theory can thus establish (categorical) properties of C(A, F) which may be used in type theory. We also show that Aczel's model construction may be extended to include the elements of any setoid as atoms or urelements. As a byproduct we obtain a natural extension of CZF, adding atoms. This extension, CZFU, is validated by the extended model. The main theorems of the paper have been checked in the proof assistant Coq which is based on MLTT. A possible application of this development is to integrate set-theoretic and type-theoretic reasoning in proof assistants.


    Volume: Volume 10, Issue 3
    Published on: September 23, 2014
    Imported on: March 25, 2013
    Keywords: Mathematics - Logic

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1789 times.
    This article's PDF has been downloaded 552 times.