[Agda] a universe of finite types

[Thorsten Altenkirch]

Hi,

thank you very much for your help!

I thought I might as well post the product of my efforts, showing that  
the family of finite sets us closed under coproducts, products and  
exponentials with the associated views. Basically (Simple) Type Theory  
for Hardware engineers...

For me it was a good way to try out the "with" mechanism which works  
very nicely (thank you, Ulf). I also realized that our remark in http://www.cs.nott.ac.uk/~txa/publ/ssgp06.pdf 
, exercise 4 was misleading, you don't need extensionality to  
implement a view on functions, because this only requires that every  
code is represented by a function and not the inverse.

I'll have a go and do Sigma and Pi instead: Hardware engineers need  
dependent types!

Cheers,
Thorsten

  
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: funi.agda
Type: application/octet-stream
Size: 3462 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20080507/7a850de4/funi-0001.obj