Add the category of predicates over agda types

[cmcmA20]

This category instance was handy when I formulated something from a paper of Conor McBride about scopes. What properties and theorems should I add?

[JacquesCarette]

Nice, thanks. Whatever properties and theorems you end up needing yourself, to ahead and submit. Small PRs are best (like this one).