Tic tac types: a gentle introduction to dependently typed programming (functional pearl). - Sean Innes; Nicolas Wu (TyDe@ICFP, 2019)