Hi Thorsten,
On Thursday 01 February 2007 08:55:30 Thorsten Altenkirch wrote:
thank you - indeed this is a very interesting observation. This was
the proof I had in mind when I first claimed that the axiom of choice
is provable in OTT. However, I was deluded in believing that OTT/
predicative
Hi Thorsten
I'm not sure I understand what's going on here.
Thorsten Altenkirch wrote:
Indeed, in the setoid model we can construct a function
f : A - [B]
--
lift f : [A - B]
if the setoid A is trivial, i.e. has the identity as its equivalence
relation.
I can
Hi Conor,
I'm not sure I understand what's going on here.
This happens if you don't type check your definitions. I got carried
away with my non-dependent simplification of the story.
Thank you for actually reading it.
Indeed, in the setoid model we can construct a function
f : A -
Hi Bas,
thank you - indeed this is a very interesting observation. This was
the proof I had in mind when I first claimed that the axiom of choice
is provable in OTT. However, I was deluded in believing that OTT/
predicative topoi exactly characterize the theory of the setoid
model. As you
