Define profunctors and representability of profunctors in 2 ways

[maxsnew]

This defines profunctors and what it means for a functor to represent a profunctor. It gives two definitions, analogous to definitions of adjunctions by hom-iso and universal morphism: Representable defines it as a functor with a hom isomorphism Hom[ F , Id ] =~ R and Representable' defines it as a function on objects F_0 with a universal morphism and induction principle (very similar to a presentation of a positive type by constructors, induction principle and beta-eta). I provided mappings between these two notions but haven't proven that it's an equivalence yet because I wasn't quite sure how to do it. My hope is that this profunctor approach can be used to flesh out the category theory part of the library, as the simplest proofs of many theorems like RAPL are structured as isomorphisms of profunctors.

This is my first time contributing to the cubical library so I'm not sure I structured it in an idiomatic way. Advice on this would be appreciated.

Related discussion in #873.

[felixwellen]

Hi Max!
We have the (rarely followed) convention, to explain what happens in a file at the beginning of the file. I think it would make sense to add your description of this PR directly as a comment, since it is certainly about concept not everyone is familiar with. Here is an example of such a comment:

https://github.com/agda/cubical/blob/master/Cubical/Foundations/Equiv/PathSplit.agda

You might want to check out the hints about whitespaces here:

https://github.com/agda/cubical/blob/master/CONTRIBUTING.md

Maybe you already found this file:

https://github.com/agda/cubical/blob/master/Cubical/Algebra/NAMING.md

On a first glance, your code looks like you are already aware of this - I'm not too familiar with the category theory part of the library and will wait a bit to give @mortberg a chance to look at your PR in more detail.

[plt-amy]

(FWIW, PRs from new contributors need approval for every commit. I've approved this latest one)

[felixwellen]

Thanks for the contribution!
Looks good to me - I only have some comments/suggestions on formatting and things like that.
There is one additional issue: In the case of putting something into a folder, like Categories/Profunctor/Base.agda, we always have a Categories/Profunctor.agda, which just imports the defaults (Profunctor/Base in this case) publicly. Please add a file like that (there should be lots of examples).

[maxsnew]

Ok I updated it with the notation I mentioned and added the Profunctor.agda file. Let me know if there's anything else

[felixwellen]

No - looks all good to me! -> Merging...