Change search
ReferencesLink to record
Permanent link

Direct link
Constructing categories and setoids of setoids in type theory
Stockholm University, Faculty of Science, Department of Mathematics.
Stockholm University, Faculty of Science, Department of Mathematics. (Matematisk logik)
2014 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, Vol. 10, no 3, 25- p.Article in journal (Refereed) Published
Abstract [en]

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

Place, publisher, year, edition, pages
2014. Vol. 10, no 3, 25- p.
Keyword [en]
Dependent type theory, setoids, formalization, categories, constructive set theory
National Category
Algebra and Logic
Research subject
Mathematical Logic
URN: urn:nbn:se:su:diva-109113DOI: 10.2168/LMCS-10(3:25)2014ISI: 000347714800022OAI: diva2:762811
(Dnr 621-2008-5076) from the Swedish Research Council (VR)
Swedish Research Council, 621-2008-5076
Available from: 2014-11-13 Created: 2014-11-13 Last updated: 2015-02-25Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Palmgren, Erik
By organisation
Department of Mathematics
In the same journal
Logical Methods in Computer Science
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 19 hits
ReferencesLink to record
Permanent link

Direct link