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

lmcs:964 - Logical Methods in Computer Science, September 23, 2014, Volume 10, Issue 3
Constructing categories and setoids of setoids in type theory

Authors: Palmgren, Erik and Wilander, Olov

In this paper we consider the problem of building rich categories of setoids, in standard intensional Martin-L\"of 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.


Source : oai:arXiv.org:1408.1364
DOI : 10.2168/LMCS-10(3:25)2014
Volume: Volume 10, Issue 3
Published on: September 23, 2014
Submitted on: March 25, 2013
Keywords: Mathematics - Logic


Share

Consultation statistics

This page has been seen 81 times.
This article's PDF has been downloaded 39 times.