Define adjunctions

[sjoerdvisscher]

No description provided.

[marcosh]

nice! adjunctions were one on those things I felt were really missing

[mstn]

Hi, I started to work on it. I do not remember why I did not finish it. If you do not have anything yet, I can have a look again.

[sjoerdvisscher]

@mstn We now have this: https://github.com/statebox/idris-ct/blob/master/idris2/Basic/Adjunction.idr

This compiles in Idris-2, but this definition throws the Idris-1 compiler in an infinite loop, and similarly other definitions were either looping or just incredibly slow, so I gave up.

So it would be interesting to see what you have!

[mstn]

I'll open a throw-away PR in next days. My definition is "less compact" and should be from Burstall's book. If I remember, I had some compilation problems as well. What I did is to unfold the natural transformation (not so elegant maybe).

Btw, what is the state of idris 2?

[sjoerdvisscher]

Inelegant code is better than code that doesn't compile!

Idris 2 is still very much in flux, and is missing a lot of features still, but it is actually working very well for idris-ct code. So it is useful for experimenting when Idris 1 is uncooperative.