\section{Related Work}

Oleg~\cite{mcbride-thesis} as inspiration. \Epigram{}~\cite{view-left}.
How does Agda~\cite{norell-thesis} work?
Earlier \Idris{}, with \Ivor{}~\cite{ivor}.

Comparison with GHC's type system and type checker.

\section{Conclusion}