My paper below includes an (implicit) recipe for interpreting set theory in a model of type theory.
Michael P. Fourman. Sheaf models for set theory. Journal of Pure and Applied Alegebra, 19:91101, 1980. @ARTICLE{fourman80, AUTHOR = {Michael P. Fourman}, TITLE = {Sheaf Models for Set Theory}, PAGES = {91101}, JOURNAL = {Journal of Pure and Applied Alegebra}, VOLUME = {19}, YEAR = {1980} } On 24 Apr 2006, at 14:30, Tjark Weber wrote: Robert,
On Sunday 23 April 2006 06:35, Robert Lamar wrote:  Do you want to prove this on paper, or in Isabelle? In any case, what  would be your theory for this proof?
My goal is a mathematical paperproof that shows that the ring theory in Isabelle is equivalent to what has been developed in Abstract Algebra. [...]
The proof that I seek, upto my understanding of the discipline, is to declare the category of rings based on ZF sets and the category of rings based on Isabelle sets, and then to find a functor from one to the other which satisfies certain requirements.
it may be conceptually simpler to look at (the categories of) arbitrary ZF sets and HOL types first. Do you consider them to be "equivalent" in any sense? Rings should then form a particular subcategory.
The embedding of type theory into ZF that you discuss in Section 3.6 of your research proposal [1] is probably going to be the usual settheoretic semantics of HOL.
Best, Tjark
