Related papers: Cartesian closed 2-categories and permutation equi…

The cartesian structure possessed by relations, spans, profunctors, and other such morphisms is elegantly expressed by universal properties in double categories. Though cartesian double categories were inspired in part by the older program…

We introduce proof terms for string rewrite systems and, using these, show that various notions of equivalence on reductions known from the literature can be viewed as different perspectives on the notion of causal equivalence. In…

Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories,…

This paper is concentrated on the classification of permutation matrix with the permutation similarity relation, mainly about the canonical form of a permutational similar equivalence class, the cycle matrix decomposition of a permutation…

A survey is given of results about coherence for categories with finite products and coproducts. For these results, which were published previously by the authors in several places, some formulations and proofs are here corrected, and…

It is proved that equalities between arrows assumed for cartesian categories are maximal in the sense that extending them with any new equality in the language of free cartesian categories collapses a cartesian category into a preorder. An…

We prove a general congruence result for bisimilarity in higher-order languages, which generalises previous work to languages specified by a labelled transition system in which programs may occur as labels, and which may rely on operations…

We revisit the definition of Cartesian differential categories, showing that a slightly more general version is useful for a number of reasons. As one application, we show that these general differential categories are comonadic over…

Relational structures are emerging as ubiquitous mathematical machinery in the semantics of open systems of various kinds. Cartesian bicategories are a well-known categorical algebra of relations that has proved especially useful in recent…

We define a tensor product for permutative categories and prove a number of key properties. We show that this product makes the 2-category of permutative categories closed symmetric monoidal as a bicategory.

We verify a confluence result for the rewriting calculus of the linear category introduced in our previous paper. Together with the termination result proved therein, the generalized coherence theorem for linear category is established.…

We consider a large family of equivalence relations on permutations in Sn that generalise those discovered by Knuth in his study of the Robinson-Schensted correspondence. In our most general setting, two permutations are equivalent if one…

We present an approach to modeling computational calculi using higher category theory. Specifically we present a fully abstract semantics for the pi-calculus. The interpretation is consistent with Curry-Howard, interpreting terms as typed…

The present paper gives a generalization of cartesian closed categories, called cartesian closed categories with dependence, whose strict version induces categories with families that support 1-, Sigma- and Pi-types in the strict sense.…

Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting…

In this paper we go into the study of 2-limits and 2-colimits in the 2-category CAT the category of small categories. More precisely we show the commutation of filtered 2-colimits and finite 2-limits. It is a generalization of a classical…

Everyone knows that if you have a bivariant homology theory satisfying a base change formula, you get an representation of a category of correspondences. For theories in which the covariant and contravariant transfer maps are in mutual…

Coherence is here demonstrated for sesquicartesian categories, which are categories with nonempty finite products and arbitrary finite sums, including the empty sum, where moreover the first and the second projection from the product of the…

We give a 3-universal property for the Karoubi envelope of a 2-category. Using this, we show that the 3-categories of finite semisimple 2-categories (as introduced in arXiv:1812.11933) and of multifusion categories are equivalent.

In this paper we study loops, neardomains and nearfields from a categorical point of view. By choosing the right kind of morphisms, we can show that the category of neardomains is equivalent to the category of sharply 2-transitive groups.…