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/ > predicat

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 ca

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 clearl