14 citations · 34 across the 9 of their papers we have counts for
10 papers
From type theory to setoids and back
Erik Palmgren
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,…
Exact completion and constructive theories of sets
Jacopo Emmenegger, Erik Palmgren
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 Constru…
On equality of objects in categories in constructive type theory
Erik Palmgren
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-ca…
A Constructive Examination of a Russell-style Ramified Type Theory
Erik Palmgren
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 pre…
Categories with families and first-order logic with dependent sorts
Erik Palmgren
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…
Constructing categories and setoids of setoids in type theory
Erik Palmgren, Olov Wilander
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…
Yet another category of setoids with equality on objects
Erik Palmgren
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…
Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets
Erik Palmgren
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…
Metric complements of overt closed sets
Thierry Coquand, Erik Palmgren, Bas Spitters
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, c…
Internalising modified realisability in constructive type theory
Erik Palmgren
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 i…