agda-categories
agda-categories copied to clipboard
[draft] Add definition of an adjunction in Bicategory
Hoping to get some feedback on design decisions. I am still planning to prove that this gives an equivalence in terms of hom-categories. If there is anything else that should be included feel free to let me know.
@Boarders this was really good - a couple of small changes, and it's ready to go in. Will you be able to do there? Or would like us to?
@JacquesCarette Sorry for the delay, I'll be happy to get this finished soon (give me a week or so as I have a current knee injury which makes too much time at the computer somewhat tricky)
No worries! I'm patient and not in a hurry. Don't strain your knee for this.