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
Hi Thorsten and others,
On Tuesday 30 January 2007 21:22:53 [EMAIL PROTECTED] wrote:
I do indeed think that Observational Type Theory with quotient types should
be the language of a Predicative Topos. I don't see in the moment that the
setoid model would introduce anything which isn't provable
Thanks to all who replied.
I have another couple of questions, more fundamental this time.
The paper says Observational reasoning can be simulated in Intensional
Type Theory by the use of setoids, i.e. types with an explicit
equivalence relation.
I'm not clear on what the differences are
Hi Robin,
thank you for your comments. Indeed we are currently revising this
paper, hence your comments are especially welcome.
I've been reading Towards Observational Type Theory. I'm new to type
theory, so I have not been able to understand big chunks of the paper;
hopefully as I read
Hi Robin,
I just saw Thorsten answered your e-mail. I'd better finish what I
started though.
I'm not an expert on OTT, but here are a few thoughts.
The real rule for coercion is the one on page 3. It doesn't require
the types to be definitionally equal. Section 5 mainly speculates on
