During the talk we used Agda to play with dependent types and better understand their meaning.
Video and source code after the jump.
I visited it following a very good recommendation. It is as much Kraftwerk retropective as a thoughtful reflection on the last 100 years of world history.
Everything starts somewhere, although many physicists disagree.
But people have always been dimly aware of the problem with the start of things. They wonder aloud how the snowplow driver gets to work, or how the makers of dictionaries look up the spellings of the words. Yet there is the constant desire to find some point in the twisting, knotting, raveling nets of space-time on which a metaphorical finger can be put to indicate that here, here, is the point where it all began…
Terry Pratchett, Hogfather