Constructing categories and setoids of setoids in type theory

TL;DR

This paper explores constructing rich categories of setoids within intensional Martin-Löf type theory, linking set-theoretic models with type-theoretic frameworks, and extending CZF with atoms validated in Coq.

Contribution

It introduces methods to build large families of setoids in type theory, connects these with set-theoretic models, and extends CZF to include atoms, all validated in Coq.

Findings

Categories of setoids can be constructed with rich structures.

Set-theoretic models can inform categorical properties in type theory.

Extension of CZF with atoms is validated by models.

Abstract

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.