A database of categories
リビジョン | 8a15f5187e74d3534ae11144f268dfc0ae7f2e3e (tree) |
---|---|
日時 | 2021-09-24 03:29:48 |
作者 | Corbin <cds@corb...> |
コミッター | Corbin |
Factor 2-categories to their own table, and format their row.
@@ -0,0 +1,25 @@ | ||
1 | +{% extends "default:row.html" %} | |
2 | + | |
3 | +{% block content %} | |
4 | + | |
5 | +{% set name = display_rows[0]["name"] %} | |
6 | +{% set cat_rows = sql("select * from categories where name = ?", [name]) %} | |
7 | +{% set objects = cat_rows[0]["objects_hr"] %} | |
8 | +{% set arrows = cat_rows[0]["arrows_hr"] %} | |
9 | +{% set transforms = display_rows[0]["transformations_hr"] %} | |
10 | +{% set strict = display_rows[0]["is_strict"] %} | |
11 | + | |
12 | +<h1>2-Category: {{ name }}</h1> | |
13 | + | |
14 | +<p>{{ name }} is the 2-category whose objects are {{ objects }}, arrows are | |
15 | +{{ arrows }}, and transformations are {{ transforms }}. Specifically, | |
16 | +{{ name }} is a | |
17 | +{% if strict %} | |
18 | +strict 2-category. | |
19 | +{% else %} | |
20 | +bicategory. | |
21 | +{% endif %} | |
22 | +</p> | |
23 | + | |
24 | +{{ super() }} | |
25 | +{% endblock %} |
@@ -22,9 +22,7 @@ | ||
22 | 22 | {% if sql("select 1 from is_locally_small where name = ?", [name]) %} |
23 | 23 | <p>{{ name }} is locally small (enriched in Set).</p> |
24 | 24 | {% endif %} |
25 | -{% if sql("select 1 from enrichments where category = ? and homs = 'Cat'", [name]) %} | |
26 | -<p>{{ name }} is a 2-category (enriched in Cat).</p> | |
27 | -{% elif sql("select 1 from enrichments where category = ? and homs = 'Pos'", [name]) %} | |
25 | +{% if sql("select 1 from enrichments where category = ? and homs = 'Pos'", [name]) %} | |
28 | 26 | <p>{{ name }} is a 2-poset, a locally posetal or 2-thin 2-category (enriched |
29 | 27 | in Pos).</p> |
30 | 28 | {% endif %} |
@@ -5,18 +5,18 @@ | ||
5 | 5 | <h1>†-categories</h1> |
6 | 6 | |
7 | 7 | <p>A †-category ("dagger category") is like a category where composition can |
8 | -happen in either direction. More precisely, the arrows of a †-category can | |
9 | -freely interchange their source and target objects. Intuitively, composition | |
10 | -in a category must follow a directed path, but composition in a †-category is | |
11 | -undirected.</p> | |
12 | - | |
13 | -<p>A †-functor ("dagger functor") is like a functor, but with an additional | |
14 | -rule for commuting everything. There is a 2-category DagCat of †-categories, | |
15 | -†-functors, and natural transformations.</p> | |
16 | - | |
17 | -<p>There is no canonical forgetful 2-functor from †-categories to | |
18 | -categories. For any particular choice of arrow direction, there is a | |
19 | -2-functor U which sends each †-category to a category:</p> | |
8 | +happen in either direction. More precisely, the arrows of a category are | |
9 | +ordered pairs of objects, but the arrows of a †-category are unordered pairs. | |
10 | +Intuitively, composition in a category must follow a directed path, but | |
11 | +composition in a †-category creates undirected paths.</p> | |
12 | + | |
13 | +<p>A †-functor ("dagger functor") is like a functor, but for arrows of | |
14 | +†-categories. There is a 2-category DagCat of †-categories, †-functors, and | |
15 | +natural transformations.</p> | |
16 | + | |
17 | +<p>There is no canonical forgetful 2-functor from †-categories to categories, | |
18 | +but there is a forgetful functor U which sends each †-category to a | |
19 | +category:</p> | |
20 | 20 | |
21 | 21 | <div class="bigmath"> |
22 | 22 | U : DagCat → Cat |
@@ -16,17 +16,15 @@ | ||
16 | 16 | constant e ~ 2.718 |
17 | 17 | * Functor categories: structure types, ... |
18 | 18 | * Presheaf categories: FinSet, Species, ... |
19 | - * The span construction: Span(Set) and Span(Grpd) are 2-categories! | |
19 | + * The span construction: Span(Set) and Span(Grpd) are 2-categories because | |
20 | + Set and Grpd have pullbacks | |
20 | 21 | * The homotopy-category construction: Ho(Cat), Ho(Top), ... |
21 | 22 | * Arrow categories: Sierpinski topos, ... |
22 | 23 | * Topoi <-> categories of sheaves on spaces |
23 | 24 | * CCCs: DagCat, ... |
24 | 25 | * Dismantle `enrichments` |
25 | 26 | * Already banned: Set, Cat |
26 | - * Give 2-categories their own table and `natural_transformations_hr` for | |
27 | - a row template page | |
28 | 27 | * Manage Evil |
29 | - * 2-categories are more Evil than bicategories | |
30 | 28 | * Double categories should be weak by default |
31 | 29 | * Upstream work |
32 | 30 | * Indexing for categories: Field, nCob, Vect_k, Mat_R, Mod(Ab) |
@@ -40,6 +38,7 @@ | ||
40 | 38 | * Shutt expressiveness: Create |
41 | 39 | * Shutt abstraction: Create |
42 | 40 | * meros: Create |
41 | + * categorical combinators: Create | |
43 | 42 | * Theorems for Free!: This should be on nLab, shouldn't it? |
44 | 43 | * Haskell: Add links |
45 | 44 | https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf and |