implement morphisms

[andrevidela]

We already have morphisms as a pair of f : a -> b, b : (x : a) -> b' (f x) -> a' x but structural typing is a bit too brittle to decompose multiple morphisms composed together