search

statebox / idris-ct

formally verified category theory library
GNU Affero General Public License v3.0
259 stars 23 forks source link

Define adjunctions #57

Open sjoerdvisscher opened 5 years ago

marcosh commented 5 years ago

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

mstn commented 5 years ago

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

@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 commented 5 years ago

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

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.