End of lecture today:

"So if anyone doesn't have anything better to do over break, I'm going to eventually assign reading *Towards Observational Type Theory*, by Conor McBride.
Also, all the proofs in *The Little Typer* should now seem trivial, if you need more general examples of dependent types.

"Make sure to have Agda 2.6.2 installed before next lecture.

"Also, if you have nothing better to do over break, you could read Homestuck. I'm not sure why you would. But you definitely could."