Three items still to be done in Functor.v

- app_associativity
- Monad_Compose
- compatible_4