Pointers needed in extensions to Martin-Lof type theory

To: caplan@cs.uiuc.edu
Subject: Pointers needed in extensions to Martin-Lof type theory
From: otto@triples.Math.McGill.CA (James Otto)
Date: Mon, 28 Feb 94 14:02:20 EST
Approved: types@dcs.gla.ac.uk


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