nmap package:constraints

This functor is fully faithful, which is to say that given any function you can write Dict a -> Dict b there also exists an entailment a :- b in the category of constraints that you can build.