fouche

icon indicating a website link http://tetrapharmakon.github.io

icon company https://compose.ioc.ee icon location Tallinn, Estonia icon location Category theorist, coend sifu. Member of https://compose.ioc.ee

Results 3 issues of fouche

Create Adjunctions.agda

3 comment

The category of adjunctions splitting a given monad, and proof that `Kleisli` and `EilenbergMoore` are initial and terminal in it.

Yoneda is broken

6 comment

The following code containing only a few imports ``` open import Categories.Category.Core open import Level module Categories.Adjoint.Duploid {o l e} {C D : Category o l e} where open import...

Isbell duality is missing

6 comment

I noticed there is no mention of Isbell duality in agda-categories https://ncatlab.org/nlab/show/Isbell+duality If you confirm me that this adjunction is not already present under a different name, hopefully a PR...