Today we discussed a type checker for simply typed lambda calculus written in Agda that Ulf Norell presented in his ICFP 2013 invited talk. Another version can be found in The view from the left by Conor McBride and James McKinna.
Last Friday, the 18th of October, I talked about homotopy and the fundamental group. As I heard about homotopy type theory, I thought that reviewing what I know of the geometric part could be useful. So I prepared this talk, using Allen Hatcher’s free textbook.
Consider a continuous line on the whiteboard, from point 
Theory Lunch 