agda
Isbell duality is missing
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?
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?
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)$...
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!
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 ☹️
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.
Yeah; things get really nasty when you have nested (co)ends, which is exactly what you need for Isabelle duality.