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:

Total : RCat → Cat

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:

Dc : RCat → DblCat

1 row where partial_category = "Pfn"

View and edit SQL

Link total_subcategory partial_category
Set Pfn

Advanced export

JSON shape: default, array, newline-delimited, object

CSV options:

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
);