Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
The page on inductive-inductive types refers to dialgebras without specifying them. Having a short page as some sort of reference is helpful.
Thanks!
In the recent $n$Lab discussions on quantum modal logic, wasn’t the need for some construction like a dialgebra, $F(x) \to G(x)$, expressed?
Or was it perhaps to what would be the morphisms in the Kleisli set-up, $F(x) \to G(y)$? Perhaps a ’diKleisli morphism’?
I ended up not seeming to have use for it after all, but a couple (literally) of references on the “two-sided Kleisli category” are since being referenced there.
I haven’t thought about relating this to di-morphisms, but it seems suggestive.
Added a reference
A dialgebraic account of labeled transition systems is in
- Fabrizio Montesi, Marco Peressotti, Linear Logic, the $\pi$-calculus, and their Metatheory: A Recipe for Proofs as Processes (arXiv:2106.11818)
And also
One more
1 to 11 of 11