ABSTRACT
The attention paid to type theory is largely for the sake of concreteness. §4 applies also to other approaches (dealing say, with (s)), and can, up to a point, be read independently of the two preceding sections. Interest in the general line investigated in §§2 and 3 does, however, seem to be growing — witness,
for instance, Ahn and Kolb [2], Kamareddine and Klein [15], Fox [13], Krause [21], Borghuis [6], Krahmer and Piwek [20], Cooper [7], Ranta [26] — and it is natural to relate this to explicit mathematics (Feferman [8]). Explicit mathematics provides in §2 the basis for an answer to (Q2) as well as a transparent treatment of subtypes, without any need for type coercion.1
