### Re: [Epigram] Definitional equality in observational type theory

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

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

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

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

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

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

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

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

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

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