This talk was given by Thorsten Altenkirch at Lambda Days, a Π type is an infinite product. He runs through typing disciplines, what dependent types are, Pre-Newtonian dependent types and what you can do with a Π type which you cannot with other types...
This talk was given by Thorsten Altenkirch at Lambda Days.