MGS14 being the lecture code and exercises for Dependently Typed Programming at Midlands Graduate School 2014, in Nottingham