# Dependently typed type checking

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.

Consider a continuous line on the whiteboard, from point $x_0$ to point $x_1$, and another continuous line from point $y_0$ to point $y_1$. Think of a bijection between the two lines: Continue reading