Isbell duality is missing

[tetrapharmakon]

I noticed there is no mention of Isbell duality in agda-categories https://ncatlab.org/nlab/show/Isbell+duality

If you confirm me that this adjunction is not already present under a different name, hopefully a PR will soon follow

I'm thinking Categories.Adjoint.Instance.Isbell as placement, any better idea?

[JacquesCarette]

AFAIK you are correct: we've never programmed that one. That's as good a place as any for the proof. Putting the various 'pieces' in their right place may also need discussion.

Which proof do you intend to follow?

[tetrapharmakon]

At the moment I am still trying to type correctly the O functor from [C,Setoid]^o to [C^o,Setoid]: on objects, it sends the copresheaf $P$ to the presheaf $C\mapsto \hom_{[C,Setoid]}(P,yC)$ where $yC$ is Yoneda. I will have to study a little other parts of the library to find the most elegant way of defining the setoid $\hom_{[C,Setoid]}(P,yC)$...

[JacquesCarette]

I was partly hoping you'd complete the (co)end calculus facilities so as to use the 'elegant' proof... but that is perhaps wishful thinking! [I had started doing all the prerequisites, but then ran out of steam.]

If you find oddities while reading other parts of the library, please do submit issues. And tiny PRs are just as welcome as big meaty ones!

[TOTBWF]

To make (co)end calculus usable, you really need a DSL for writing "functorial forms", EG: the stuff that happens underneath the integral. If you don't have this, then things degenerate into an unreadable point-free mess of functor compositions ☹️

[JacquesCarette]

To make (co)end calculus usable, you really need a DSL for writing "functorial forms", EG: the stuff that happens underneath the integral. If you don't have this, then things degenerate into an unreadable point-free mess of functor compositions ☹️

Ah, that makes sense - need more intensionality, doing this extensionally gets all messy.

[TOTBWF]

Yeah; things get really nasty when you have nested (co)ends, which is exactly what you need for Isabelle duality.