Comment by frozenlettuce

The approach of using a function to describe a type where success is the identity is a very simple way to implement dependant types