agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
363 stars 68 forks source link

Stub for representable profunctor #318

Closed tetrapharmakon closed 2 years ago

tetrapharmakon commented 2 years ago

Any functor F : C -> D induces two "representable" profunctors

hom(F,1) : (c,d) \mapsto D(Fc,d)

and

hom(1,F) : (d,c) \mapsto D(d, Fc)