search

agda / agda-categories

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

[draft] Add definition of an adjunction in Bicategory #348

Open Boarders opened 2 years ago

Boarders commented 2 years ago

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.

JacquesCarette commented 2 years ago

@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?

Boarders commented 2 years ago

@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)

JacquesCarette commented 2 years ago

No worries! I'm patient and not in a hurry. Don't strain your knee for this.

JacquesCarette commented 8 months ago

I'd like to get this done - if you give me permission to push to your fork, I can do those small changes needed and then merge it in?