Create Adjunctions.agda #326
Conversation
The category of adjunctions splitting a given monad, and proof that `Kleisli` and `EilenbergMoore` are initial and terminal in it.
| open import Categories.Category | ||
| open import Categories.Monad | ||
|
|
||
| module Categories.Adjoint.Construction.AdjunctionTerminalInitial {o ℓ e} {C : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e} (M : Monad C) where |
There was a problem hiding this comment.
I would be tempted to call this Categories.Adjoint.Construction.Adjunctions.Properties.
|
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? |
|
We think we laid down all relevant equalities and constraints required to complete the proofs in |
|
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. |
src/Categories/Adjoint/Construction/Adjunctions/Properties.agda
Outdated
Show resolved
Hide resolved
The category of adjunctions splitting a given monad, and proof that
KleisliandEilenbergMooreare initial and terminal in it.