14 citations · 34 across the 9 of their papers we have counts for
Showing 2017Show all
3 papers · 1 filter
math.LO2017★ 5 cited
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…
math.CT2017★ 4 cited
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…
math.LO2017
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…