proved functor eq, modified its type a bit, so other things will break but need to move computers to fix completeness
modified:   Functors.agda
modified:   Utilities.agda