Hello, I know there are many haskellers interested in dependent type theory so I wanted to mention that there is now an IRC channel on freenode for discussing Homotopy Type Theory (HoTT), e.g., the recent book, possible implementations, dependent type theory in general, etc. The channel is ##hott (NOTE the *two* hashes!) and you can connect directly through freenode's web interface if you don't already have a client: https://webchat.freenode.net/?channels=%23%23hott Currently we have around 50 members but the more the merrier! If you don't know much about IRC but would like to learn more: * http://www.irchelp.org — how IRC works, software clients, FAQs, and other info * http://freenode.net — info about the freenode IRC network specifically Cheers, Darin Morrison