Many thanks to those who responded to my questions. Here's a short summary of th replies. best, steve ------------------------------------------------------------ 1. Relationship with Martin-Löf types: a. B. Jacobs. *Categorical Logic and Type Theory*. Elsevier. 1998. b. @Article{Seely84, author = "R. A. G. Seely", title = "Locally Cartesian Closed Categories and Type Theory", journal = "Math. Proc. Cambridge Philos. Soc.", volume = "95", pages = "33--48", year = "1984", } 2. Computer systems a. FISh, http://www-staff.socs.uts.edu.au/~cbj/FISh and www-staff.it.uts.edu.au/~cbj/Publications/constructors.ps b. IFF Foundation Ontology, http://suo.ieee.org/Kent-IFF.pdf c. David Rydeheard provided a pointer to the code for *Computational Category Theory*, http://www.cs.man.ac.uk/~david/categories/code/ d. Charity, http://www.cpsc.ucalgary.ca/projects/charity/home.html