[draft] Add definition of an adjunction in Bicategory #348
Conversation
|
|
||
| record Adjunction (A B : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ t) where | ||
| private | ||
| module C = Extras 𝒞 |
There was a problem hiding this comment.
We should probably pull this module out of the record, and into the enclosing module.
There was a problem hiding this comment.
Yes. And may as well open it extracting the unitors and ≈.
| r-triangle-r : id₁ ⊚₀ R ⇒₂ R | ||
| r-triangle-r = C.unitorˡ.from | ||
| field | ||
| l-triangle : l-triangle-l C.≈ l-triangle-r |
There was a problem hiding this comment.
Perhaps we should name these zig and zag for alignment with Categories.Adjoint.
There was a problem hiding this comment.
Agree with @TOTBWF : looks good, but a couple of tweaks would make it even better, and ready for inclusion.
|
|
||
| record Adjunction (A B : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ t) where | ||
| private | ||
| module C = Extras 𝒞 |
There was a problem hiding this comment.
Yes. And may as well open it extracting the unitors and ≈.
| r-triangle-r : id₁ ⊚₀ R ⇒₂ R | ||
| r-triangle-r = C.unitorˡ.from | ||
| field | ||
| l-triangle : l-triangle-l C.≈ l-triangle-r |
|
@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. |
|
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? |
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.