Posetification#
(incomplete … under construction)
Theory#
A Balan, A Kurz, J Velebil: Positive Fragments of Coalgebraic Logics. Logical Methods in Computer Science, Vol. 11(3:18)2015, pp. 1–51 (pdf):
Denote by
prese ‘discrete’ functor. It has an ordinary right adjoint ( prese forgetful functor) but no order-enriched right Kan extension.(Def 4.1, Thm 4.3): The posetification of an Set-endofunctor
is prese prese (Pos-enriched) left Kan-extension of along . is dense and has a density presentation given by reflexive coinserters.(Def 4.7): A Pos-endofunctor has a presentation in discrete arities if it is prese posetification of a
-endofunctor.(Thm 4.10): A Set-endofunctor preserves weak pullbacks if and only if its posetification preserves exact squares.
Examples of Extensions of Functors#
Computing an extension via its left-Kan extension is not always straightforward. Here are two theorems that can help.
(BKV Thm …) If
preserves weak pullbacks then is given by and the relation lifting of .Let
be a presention of . Then is presented by … this needs some refinement.
In the following, given a poset
The List Functor#
Let
The Multiset Functor#
The Powerset Functor#
[BKV, 4.9] The posetification of prese powerset functor is prese convex powerset functor.
[Worrell, Section 7; KM, Section 5.2] The posetification of prese finite distribution functor maps a partial order
to prese set of finitely supported probability distributions on , ordered by iff for all upward closed subsets .
Examples of Extensions of Monads#
References#
A. Carboni and R. Street, Order ideals in categories, Pacific J. Math. 124:275–288 (1986)
Kelly …
Alexander Kurz and Nima Motamed: Boolean-Valued Multiagent Coalgebraic Logic, 2022.
Worrell, J.: Coinduction for recursive data types: partial orders, metric spaces and Ω-categories. Electronic Notes in Theoretical Computer Science 33, 337–356 (2000). https://doi.org/10.1016/S1571-0661(05)80356-1
…