Date: Wed, 15 Jun 1994 14:18:17 +0500 (GMT+4:00)
Subject: McCarty = Eff

Date: Wed, 15 Jun 94 16:04:02 +0200
From: Thomas Streicher <streiche@informatik.uni-muenchen.de>

Recently in a discussion with J. Lipton there came up the question
whether the full and faithful embedding of D. McCarty's realisability
model of IZF into the effective topos  Eff   is actually an
equivalence. More concretely that means whether any object of the
effective topos is really isomorphic to an object of the McCarty
topos. I think the problem is highly nontrivial as the equality
predicate on an object of the McCarty topos is derived form its
inductive presentation.
I would be pleased in any comments. Thanks in advance,

Thomas Streicher