search

agda / agda-categories

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

Create Adjunctions.agda #326

Open tetrapharmakon opened 2 years ago

tetrapharmakon commented 2 years ago

The category of adjunctions splitting a given monad, and proof that Kleisli and EilenbergMoore are initial and terminal in it.

JacquesCarette commented 2 years ago

This was a good start @tetrapharmakon . Ready to come back to this and 'finish' it? Is there something I can do to help that along?

iwilare commented 2 years ago

We think we laid down all relevant equalities and constraints required to complete the proofs in Adjunctions.Properties. The remaining proof for homomorphism certainly looks like a hard journey to complete; perhaps you can see some easier way to close this?

JacquesCarette commented 2 years ago

I think what makes sense to do would to be to do this in phases: first the basic construction (which is done), then its properties (in progress). I could comment out the unfinished bits and bring the rest in now.

I can then look to see if I have ideas on how to complete the holes.