Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Thorsten Altenkirch
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

Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Bas Spitters
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

Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Conor McBride
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

Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Thorsten Altenkirch
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 -

Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Thorsten Altenkirch
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

Re: [Epigram] Definitional equality in observational type theory

2007-01-31 Thread Bas Spitters
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

Re: [Epigram] Definitional equality in observational type theory

2007-01-29 Thread Thorsten Altenkirch
Hi Robin, 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 between OTT and simulating observational reasoning with setoids in ITT. Clearly OTT

Re: [Epigram] Definitional equality in observational type theory

2007-01-29 Thread Bas Spitters
Dear Thorsten, Robin, Now that the discussion has turned to setoids and observational type theory, I could not help myself from responding. (Thorsten and I had quite some off-line discussion about this). I generally agree with Thorsten's description of observational type theory as

Re: [Epigram] Definitional equality in observational type theory

2007-01-26 Thread Robin Green
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

Re: [Epigram] Definitional equality in observational type theory

2007-01-25 Thread Thorsten Altenkirch
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

Re: [Epigram] Definitional equality in observational type theory

2007-01-25 Thread Wouter Swierstra
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