### Re: [Epigram] Meeting A) or B)

. Will confirm. James. -- Dr. Thorsten Altenkirchphone : (+44) (0)115 84 66516 Lecturer http://www.cs.nott.ac.uk/~txa/ School of Computer Science ITUniversity of Nottingham This message has been scanned but we cannot guarantee that it and any attachments are free

### Re: [Epigram] Epigram and Type:Type

Adam Megacz wrote: Thorsten Altenkirch [EMAIL PROTECTED] writes: What is Gilmore's ITT (is this Stephen Gilmore, is he doing Types these days)? http://www.cs.ubc.ca/spider/gilmore/ http://www.megacz.com/research/papers/logicism.renewed.notes.pdf To address the problems, we have in the past

### Re: [Epigram] zero not suc

at 6.1 of http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf Can you complete that proof? Yes, ( n : Nat ! let !--! ! zeronosuc n : not (zero = suc n) ) zeronosuc n = znosuc n Cheers, Thorsten -- Dr. Thorsten Altenkirch

### Re: [Epigram] a naught E, non-structural call

Conor McBride wrote: Hi Sebastian Sebastian Hanowski wrote: ( f : Fin (suc m) - Fin (suc n) ! let !---! ! restrict _m _n f : Fin m - Fin n ) Should you be able to write a function with this type? I can certainly write a function from Fin 2 to

### Re: [Epigram] Why does not Epigram accept this?

Hi Lars, Sorry for the disturbance I cause but I still can not get the pairglob function right it seems. The definition I sent you a few days ago used a case construction which is unneccesary in the presence of the selectors (eliminators) globroot and globchild. So I wrote a new pairglob using

### Re: [Epigram] epigram tells me fibs

elimnators using well known techniques. Cheers, Thorsten -- Dr. Thorsten Altenkirchphone : (+44) (0)115 84 66516 Lecturer http://www.cs.nott.ac.uk/~txa/ School of Computer Science ITUniversity of Nottingham This message has been checked for viruses

### Re: [Epigram] epigram tells me fibs

Yong Luo wrote: Hi, Conor, Since you use elimination rule on both arguments, I was expecting four cases like Thorsten did in the previous email. If you can define the Ackermann function, then you must be able to define the Majority function. Is there anything more than the standard

### Re: [Epigram] epigram tells me fibs

Since you use elimination rule on both arguments, I was expecting four cases like Thorsten did in the previous email. Can we define the Ackermann function like the following form? Conor used the official version of the Ackermann function, which just has three lines, while I used my own

### Re: [Epigram] epigram tells me fibs

Apologies, this email was intended for Yong personally - not for the list. My mistake. Thorsten Thorsten Altenkirch wrote: Yong Luo wrote: Hi, Conor, Since you use elimination rule on both arguments, I was expecting four cases like Thorsten did in the previous email. If you can define

### 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, 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

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

### [Epigram] CFP: Dependently Typed Programming (FI Special Issue)

(http://sneezy.cs.nott.ac.uk/darcs/DTP08/journal.html) Editors: Thorsten Altenkirch (Nottingham) Tarmo Uustalu (Tallinn) Dependently typed programming is using the power of dependent types to capture relationships between data

### [Epigram] PhD positions at Nottingham Swansea

Hi, we have two fully funded PhD positions in our project on induction- recursion: one at Swansea (with Anton Setzer) and one at Nottingham (with me). This would be perfect for people who are interested in the foundations of Type Theory. See http://www.cs.nott.ac.uk/~txa/phd.html Please