agda / agda-categories

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

Parametric adjunctions form cowedges #360

Closed iwilare closed 1 year ago

iwilare commented 1 year ago

We define the notion of parametric adjunction Lc ⊣ Rc between functors L : C x D → E and R : Cᵒ x E → D and show that, under suitable assumptions, the counit of the adjunction ε[c,x] : L(c,R(c,x)) → x is a cowedge in the parameter c.

For more information consult this question on StackExchange.

j.w.w. @tetrapharmakon