Restriction Categories

A restriction category is a category with a restriction operator which restricts each arrow to a subdomain. By analogy, the original category's arrows are partial, but the arrows of the subcategory obtained by restricting every arrow are total.

The restriction operator extends to a functor from restriction categories to categories:

Additionally, every restriction category forms a double category whose vertical arrows are the original partial arrows and horizontal arrows are the restricted total arrows. This construction also extends to a functor from restriction categories to double categories:

1 row where total_subcategory = "Set"

✎ View and edit SQL

This data as json, CSV (advanced)

CREATE TABLE "restriction_categories" (
	"total_subcategory"	TEXT NOT NULL,
	"partial_category"	TEXT NOT NULL,
	FOREIGN KEY("total_subcategory") REFERENCES "categories"("name") on update cascade on delete restrict,
	PRIMARY KEY("partial_category","total_subcategory"),
	FOREIGN KEY("partial_category") REFERENCES "categories"("name") on update cascade on delete restrict
);