search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
454 stars 139 forks source link

Define profunctors and representability of profunctors in 2 ways #945

Closed maxsnew closed 1 year ago

maxsnew commented 2 years ago

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 https://github.com/agda/cubical/pull/873.

felixwellen commented 2 years ago

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 commented 2 years ago

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

maxsnew commented 1 year ago

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

felixwellen commented 1 year ago

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