Began work on translating hask ideas into Coq

Starting with Univariance.hs -> Functors.v