[Prev][Next][Index][Thread]
Pointers needed in extensions to Martin-Lof type theory
dear Joshua Caplan
Has there been any more work done on partial computations and general
recursion in Martin-Lof type theory since the 1987 LICS paper of
Constable and Smith? ("Partial Objects in Constructive Type Theory,"
Proc. LICS 1987.)
i don't know if this is already there, but it is true that e.g.
$\Pi^1_1$ is representable in LCC (locally cartesian closed)
categories with NNO (natural numbers objects). there is an initial
such category I (as, with chosen structure, the specification is
essentially algebraic). in the image of the (unique up to natural
isomorphim) LCC-NNO functor from I to the category of sets, onto/into
factorizations of image maps include all the $\Pi^1_1$ relations (as
into parts).
Any references, especially anon-FTP-able ones, would be greatly
appreciated.
for ftp, sorry for now. i'll be interested in what you find. i have
a vaguely related paper (but much of how it is related remains to be
spelled out!) available by email:
The linear time hierarchy ($\Delta_0$)
via tiers and monoidal categories
bon jour, Jim Otto