†-categories

A †-category ("dagger category") is like a category where composition can happen in either direction. More precisely, the arrows of a category are ordered pairs of objects, but the arrows of a †-category are unordered pairs. Intuitively, composition in a category must follow a directed path, but composition in a †-category creates undirected paths.

A †-functor ("dagger functor") is like a functor, but for arrows of †-categories. There is a 2-category DagCat of †-categories, †-functors, and natural transformations.

There is no canonical forgetful 2-functor from †-categories to categories, but there is a forgetful functor U which sends each †-category to a category:

And equips that category with an involutive endofunctor † which is the identity on objects:

While U might not be canonical, it will always choose the same categories and involutive endofunctors up to equivalence, so we may speak of as a category without ambiguity.

The arrows of the core of a †-category are called unitary arrows.

0 rows where category = "Pfn"

✎ View and edit SQL

This data as json

0 records

CREATE TABLE "dagger_categories" (
	"category"	TEXT NOT NULL UNIQUE,
	FOREIGN KEY("category") REFERENCES "categories"("name") on update cascade on delete restrict,
	PRIMARY KEY("category")
);