The approach of using a function to describe a type where success is the identity is a very simple way to implement dependant types
For instance this might be super mario... mario moves forward or the gumba moves forward or mario hits the gumba and mario enters death animation and the gumba stops or mario hits the gumba from above and the gumba enters death animation or mario hits a coin box and a his coins increase and mario stops and the box enters coin animation.