Make it a proper Markdown-based literate Agda file (hiding imports, etc), and fix the formatting of lines with vertical vectors.