\section{Related Work}

Oleg~\cite{McBride1999} as inspiration. \Epigram{}~\cite{McBride2004a}.
How does Agda~\cite{norell2007thesis} work?
Earlier \Idris{}, with \Ivor{}~\cite{Brady2006b}.

Comparison with GHC's type system and type checker.

\section{Conclusion}