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