Murat Kasimov

More about me

Я language (β)

/Я language (β)/Operators/kyokl/

(`kx`) Source lax co-[K]leisli morphism (`yo`) [Y]oneda functor mapping c[O]variantly (`xk`) Source lax [K]leisli morphism (`xl`) Target lax K[L]eisli morphism
`kyokl` : target ( t a ) ( target ( source ( tt a ) ( ttt o )) ( ttt ( t a ) ) )

Looks like a big circle `yi` with a bullet point `ho` inside designating covariant position of a focused parameter equipped with a small left hook `kx` designating source co-Kleisli morphism, a small right hook `xk` designating source Kleisli morphism and a big hook `xl` designating target Kleisli morphism.

Original mapping of derived functor definition:

: source ( tt a ) ( ttt o )`AR____` target ( t a ) ( ttt ( t a ) )

Type declaration with labels arrangement:

`kyokl` : target ( t a ) ( target ( source ( tt a ) ( I `L` tt `T` ll `T'I` ttt `L` ttt `T` lll `L` t `T` l `T` o )) ( ttt ( t o ) ) )

Available stretched versions (starting precedence is 5):

`kyokl_`, `kyokl__`