A differential category is an additive symmetric monoidal category with an algebra modality, axiomatizing smooth functions, and a deriving transformation, axiomatizing the differentiation of these smooth functions. An algebra modality may or may not have both the nullary and the binary Seely isomorphisms. Lemay proved that if an algebra modality has both Seely isomorphisms, then it has at most one deriving transformation. It was then an open problem whether every algebra modality has at most one deriving transformation. We answer this question in the negative by constructing algebra modalities with infinite sets of deriving transformations. We also clarify the relations between the nullary Seely isomorphism, the binary Seely isomorphism, and uniqueness of deriving transformations (that is, the property for an algebra modality to have at most one deriving transformation). First, we refine Lemay's theorem by removing the assumption of the nullary Seely isomorphism. Then, we show by means of various examples that the six combinations of absence or presence of nullary Seely isomorphism, binary Seely isomorphism, and uniqueness of deriving transformations, which are not already ruled out by the refined uniqueness theorem, can be realized.
We introduce partial Markov categories as a synthetic framework for synthetic probabilistic inference, blending the work of Cho and Jacobs, Fritz, and Golubtsov on Markov categories with the work of Cockett and Lack on cartesian restriction categories. We describe observations, Bayes' theorem, normalisation, and both Pearl's and Jeffrey's updates in purely categorical terms.
Cons-lists are fundamental to functional programming, and are well-understood as initial algebras, and as a concrete construction of free monoids. In category theory, such list objects can be axiomatised internal to any monoidal category, with nil and cons maps, and a recursion mechanism. When strengthened to support parametrised recursion, they can be shown to give the free monoid construction. We study a small variant on parametrised list objects called parametrised symmetric list objects, in a symmetric monoidal category, where the two frontmost elements are allowed to be permuted. We show that this gives a construction of free commutative monoids, and develop some related theory.
We give a categorical formulation of Kraus' "magic trick" for recovering information from truncated types. Rather than type theory, we work in Van den Berg-Moerdijk path categories with a univalent universe, and rather than propositional truncation we work with arbitrary cofibrations, which includes truncation as a special case. We show, using Kraus' argument that any cofibration with homogeneous domain is a monomorphism. We give some simple concrete examples in groupoids to illustrate the interaction between homogeneous types, cofibrations and univalent fibrations.