Showing 1–10 of 10 results for author: Palmgren, E

From type theory to setoids and back

Authors: Erik Palmgren

Abstract: A model of Martin-Löf extensional type theory with universes is formalized in Agda, an interactive proof system based on Martin-Löf intensional type theory. This may be understood, we claim, as a solution to the old problem of modelling the full extensional theory in the intensional theory. Types are interpreted as setoids, and the model is therefore a setoid model. We solve the problem of intepre… ▽ More A model of Martin-Löf extensional type theory with universes is formalized in Agda, an interactive proof system based on Martin-Löf intensional type theory. This may be understood, we claim, as a solution to the old problem of modelling the full extensional theory in the intensional theory. Types are interpreted as setoids, and the model is therefore a setoid model. We solve the problem of intepreting type universes by utilizing Aczel's type of iterative sets, and show how it can be made into a setoid of small setoids containing the necessary setoid constructions. In addition we interpret the bracket types of Awodey and Bauer. Further quotient types should be interpretable. △ Less

Submitted 16 September, 2019; v1 submitted 3 September, 2019; originally announced September 2019.

Comments: 31 pages

MSC Class: 03B15; 03B35; 03E70; 03F50

Exact completion and constructive theories of sets

Authors: Jacopo Emmenegger, Erik Palmgren

Abstract: In the present paper we use the theory of exact completions to study categorical properties of small setoids in Martin-Löf type theory and, more generally, of models of the Constructive Elementary Theory of the Category of Sets, in terms of properties of their subcategories of choice objects (i.e. objects satisfying the axiom of choice). Because of these intended applications, we deal with categor… ▽ More In the present paper we use the theory of exact completions to study categorical properties of small setoids in Martin-Löf type theory and, more generally, of models of the Constructive Elementary Theory of the Category of Sets, in terms of properties of their subcategories of choice objects (i.e. objects satisfying the axiom of choice). Because of these intended applications, we deal with categories that lack equalisers and just have weak ones, but whose objects can be regarded as collections of global elements. In this context, we study the internal logic of the categories involved, and employ this analysis to give a sufficient condition for the local cartesian closure of an exact completion. Finally, we apply this result to show when an exact completion produces a model of CETCS. △ Less

Submitted 5 May, 2021; v1 submitted 29 October, 2017; originally announced October 2017.

Comments: 19 pages. v2: examples in type theory moved to a final section; to appear in J. Symb. Log. v3: arXiv abstract fixed, paper is the same as v2

MSC Class: 03B15; 18B05; 18D15; 03F55; 03G30; 18A35

Journal ref: J. Symb. Log. 85(2), 2020

On equality of objects in categories in constructive type theory

Authors: Erik Palmgren

Abstract: In this note we remark on the problem of equality of objects in categories formalized in Martin-Löf's constructive type theory. A standard notion of category in this system is E-category, where no such equality is specified. The main observation here is that there is no general extension of E-categories to categories with equality on objects, unless the principle Uniqueness of Identity Proofs (UIP… ▽ More In this note we remark on the problem of equality of objects in categories formalized in Martin-Löf's constructive type theory. A standard notion of category in this system is E-category, where no such equality is specified. The main observation here is that there is no general extension of E-categories to categories with equality on objects, unless the principle Uniqueness of Identity Proofs (UIP) holds. We also introduce the notion of an H-category, a variant of category with equality on objects, which makes it easy to compare to the notion of univalent category proposed for Univalent Type Theory by Ahrens, Kapulkin and Shulman. △ Less

Submitted 6 August, 2017; originally announced August 2017.

Comments: 7 pages

MSC Class: 18A15 03F50

Journal ref: 23rd International Conference on Types for Proofs and Programs, Art. No. 7, 7 pp., LIPIcs. Leibniz Int. Proc. Inform., 104, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2018

A Constructive Examination of a Russell-style Ramified Type Theory

Authors: Erik Palmgren

Abstract: In this paper we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell's reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematic… ▽ More In this paper we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell's reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematics. We present a ramified type theory suitable for this purpose. One may regard the results of this paper as an alternative solution to the problems of Russell's theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here, also suggests that there is a natural associated notion of predicative elementary topos. △ Less

Submitted 22 April, 2017; originally announced April 2017.

Comments: 14 pages

MSC Class: 03B15; 03F35; 03F50

Categories with families and first-order logic with dependent sorts

Authors: Erik Palmgren

Abstract: First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL), may be regarded as logic enriched dependent type theories. Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Löf type theory. We introduce in this… ▽ More First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL), may be regarded as logic enriched dependent type theories. Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Löf type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and DFOL fit in this semantical framework. A soundness and completeness theorem is proved for DFOL. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle. △ Less

Submitted 7 July, 2019; v1 submitted 5 May, 2016; originally announced May 2016.

Comments: 83 pages

MSC Class: 03B15; 03F50; 03G30; 18C10; 68Q55

Journal ref: Annals of Pure and Applied Logic Volume 170, Issue 12, December 2019

Constructing categories and setoids of setoids in type theory

Authors: Erik Palmgren, Olov Wilander

Abstract: 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 crucia… ▽ More 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. △ Less

Submitted 19 September, 2014; v1 submitted 6 August, 2014; originally announced August 2014.

Comments: 14 pages

Journal ref: Logical Methods in Computer Science, Volume 10, Issue 3 (September 23, 2014) lmcs:964

Yet another category of setoids with equality on objects

Authors: Erik Palmgren

Abstract: When formalizing mathematics in (generalized predicative) constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids (types with explicit equivalence relations). In this note we consider two categories of setoids with equality on objects and show that they are isomorphic. Both categories are constructed from a fixed proof-irrelevant family… ▽ More When formalizing mathematics in (generalized predicative) constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids (types with explicit equivalence relations). In this note we consider two categories of setoids with equality on objects and show that they are isomorphic. Both categories are constructed from a fixed proof-irrelevant family $F$ of setoids. The objects of the categories are the index setoid $I$ of the family, whereas the definition of arrows differs. The first category has for arrows triples $(a,b,f:F(a) \to F(b))$ where $f$ is an extensional function. Two such arrows are identified if appropriate composition with transportation maps (given by $F$) makes them equal. In the second category the arrows are triples $(a,b,R \hookrightarrow Σ(I,F)^2)$ where $R$ is a total functional relation between the subobjects $F(a), F(b) \hookrightarrow Σ(I,F)$ of the setoid sum of the family. This category is simpler to use as the transportation maps disappear. Moreover we also show that the full image of a category along an E-functor into an E-category is category. △ Less

Submitted 21 April, 2013; originally announced April 2013.

Comments: 13 pages

MSC Class: 03B15 03F50 18B05

Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets

Authors: Erik Palmgren

Abstract: Bishop's informal set theory is briefly discussed and compared to Lawvere's Elementary Theory of the Category of Sets (ETCS). We then present a constructive and predicative version of ETCS, whose standard model is based on the constructive type theory of Martin-Löf. The theory, CETCS, provides a structuralist foundation for constructive mathematics in the style of Bishop. Bishop's informal set theory is briefly discussed and compared to Lawvere's Elementary Theory of the Category of Sets (ETCS). We then present a constructive and predicative version of ETCS, whose standard model is based on the constructive type theory of Martin-Löf. The theory, CETCS, provides a structuralist foundation for constructive mathematics in the style of Bishop. △ Less

Submitted 30 January, 2012; originally announced January 2012.

Comments: 28 pages

MSC Class: 03B15; 03G30; 18B05; 18B25

Metric complements of overt closed sets

Authors: Thierry Coquand, Erik Palmgren, Bas Spitters

Abstract: We show that the set of points of an overt closed subspace of a metric completion of a Bishop-locally compact metric space is located. Consequently, if the subspace is, moreover, compact, then its collection of points is Bishop compact. We show that the set of points of an overt closed subspace of a metric completion of a Bishop-locally compact metric space is located. Consequently, if the subspace is, moreover, compact, then its collection of points is Bishop compact. △ Less

Submitted 18 June, 2009; originally announced June 2009.

Comments: 9 pages, 1 figure

MSC Class: 06D22; 28C05

Journal ref: Mathematical Logic Quarterly, 57(4), 373-378, 2011

Internalising modified realisability in constructive type theory

Authors: Erik Palmgren

Abstract: A modified realisability interpretation of infinitary logic is formalised and proved sound in constructive type theory (CTT). The logic considered subsumes first order logic. The interpretation makes it possible to extract programs with simplified types and to incorporate and reason about them in CTT. A modified realisability interpretation of infinitary logic is formalised and proved sound in constructive type theory (CTT). The logic considered subsumes first order logic. The interpretation makes it possible to extract programs with simplified types and to incorporate and reason about them in CTT. △ Less

Submitted 5 October, 2005; v1 submitted 19 May, 2005; originally announced May 2005.

Comments: 7 pages

ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 1, Issue 2 (October 5, 2005) lmcs:2266