Commit: 2f7600df8944b45de89d0d2aaddfe851e6407fde - catabase (git)

A database of categories

Commit MetaInfo

• Revision: 2f7600df8944b45de89d0d2aaddfe851e6407fde (tree)
• Time: 2021-09-23 03:54:38
• Author: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Clean up opposite and dagger categories.

Change Summary

• modified: catabase.db
• add: templates/row-catabase-dagger_categories.html
• modified: templates/row-catabase-opposite_categories.html
• add: templates/table-catabase-dagger_categories.html
• modified: templates/table-catabase-restriction_categories.html
• add: todo.txt

Incremental Difference

Binary files a/catabase.db and b/catabase.db differ

--- /dev/null
+++ b/templates/row-catabase-dagger_categories.html
@@ -0,0 +1,31 @@
+{% extends "default:row.html" %}
+
+{% block content %}
+
+{% set cat = display_rows[0]["category"] %}
+
+<h1>†-category: {{ cat }}</h1>
+
+<p>{{ cat }} is a †-category. Composition in {{ cat }} can happen in
+either direction; every arrow can interchange its source and target objects
+freely.</p>
+
+{% set core_rows = sql("select groupoid from cores where category = ?", [cat]) %}
+{% if core_rows %}
+{% set grpd = core_rows[0]["groupoid"] %}
+{% set unitary_rows = sql(
+"select arrows_hr from categories where name = ?", [grpd]) %}
+{% set unitary_arrows = unitary_rows[0]["arrows_hr"] %}
+<p>The core of {{ cat }} is the groupoid {{ grpd }}:</p>
+
+<div class="bigmath">
+    Core({{ cat }}) ≅ {{ grpd }}
+</div>
+
+<p>The unitary arrows of {{ cat }} are the arrows of {{ grpd }}; they are
+{{ unitary_arrows }}.</p>
+{% endif %}
+
+{{ super() }}
+{% endblock %}
+

--- a/templates/row-catabase-opposite_categories.html
+++ b/templates/row-catabase-opposite_categories.html
@@ -12,9 +12,10 @@
 {% else %}
 <h1>Opposite Categories: {{ cat }} &amp; {{ opcat }}</h1>
 
-<p>{{ cat }} and {{ opcat }} are opposites; they are equivalent, except that
-the arrows in {{ cat }} are pointed in the opposite direction from in
-{{ opcat }}.</p>
+<p>{{ cat }} and {{ opcat }} are opposites; they share the same objects,
+identity arrows, and composition, but the arrows in {{ cat }} are pointed in
+the opposite direction from in {{ opcat }}. This is a contravariant
+equivalence of categories.</p>
 {% endif %}
 
 {{ super() }}

--- /dev/null
+++ b/templates/table-catabase-dagger_categories.html
@@ -0,0 +1,39 @@
+{% extends "default:table.html" %}
+
+{% block content %}
+
+<h1>†-categories</h1>
+
+<p>A †-category ("dagger category") is like a category where composition can
+happen in either direction. More precisely, the arrows of a †-category can
+freely interchange their source and target objects. Intuitively, composition
+in a category must follow a directed path, but composition in a †-category is
+undirected.</p>
+
+<p>A †-functor ("dagger functor") is like a functor, but with an additional
+rule for commuting everything. There is a 2-category DagCat of †-categories,
+†-functors, and natural transformations.</p>
+
+<p>There is no canonical forgetful 2-functor from †-categories to
+categories. For any particular choice of arrow direction, there is a
+2-functor U which sends each †-category to a category:</p>
+
+<div class="bigmath">
+    U : DagCat → Cat
+</div>
+
+<p>And equips that category with an involutive endofunctor † which is the
+identity on objects:</p>
+
+<div class="bigmath">
+    † : X ↦ X
+</div>
+
+<p>While U might not be canonical, it will always choose the same categories
+and involutive endofunctors up to equivalence, so we may speak of {{ cat }} as
+a category without ambiguity.</p>
+
+<p>The arrows of the core of a †-category are called unitary arrows.</p>
+
+{{ super() }}
+{% endblock %}

--- a/templates/table-catabase-restriction_categories.html
+++ b/templates/table-catabase-restriction_categories.html
@@ -1,4 +1,4 @@
-{% extends "default:row.html" %}
+{% extends "default:table.html" %}
 
 {% block content %}
 

--- /dev/null
+++ b/todo.txt
@@ -0,0 +1,46 @@
+* Catabase:
+  * all_ polymorphism
+    * All skeletal subcategories are equivalences of categories;
+      maybe `all_equivalent_categories`?
+      * Would handle opposite categories too...
+    * `all_groupoids`? Would include cores and homotopy categories?
+  * Random facts not yet encodable
+    * P and FinSet are symmetric rig categories
+      * So is Vect_k, but not with categorical product
+    * MonCat has a double category, using "oplax" monoidal functors
+    * Monoidal categories in general
+      * Needs polymorphism
+      * Categorical product -> Cartesian closed
+      * Many other cases to handle
+    * The Euler characteristic AKA groupoid cardinality of P is Euler's
+      constant e ~ 2.718
+    * Functor categories: structure types, ...
+    * Presheaf categories: FinSet, Species, ...
+    * The span construction: Span(Set) and Span(Grpd) are 2-categories!
+    * The homotopy-category construction: Ho(Cat), Ho(Top), ...
+    * Arrow categories: Sierpinski topos, ...
+    * Topoi <-> categories of sheaves on spaces
+    * CCCs: DagCat, ...
+  * Dismantle `enrichments`
+    * Give 2-categories their own table and `natural_transformations_hr` for
+      a row template page
+  * Manage Evil
+    * 2-categories are more Evil than bicategories
+    * Double categories should be weak by default
+    * Dagger categories should be equipped with structure
+  * Upstream work
+    * Indexing for categories: Field, nCob, Vect_k, Mat_R, Mod(Ab)
+      * Field and nCob are disconnected by index!
+* Complexity:
+  * Refactor `is_contained_in` and `is_not_contained_in` to views
+    * Imply containment and separation using example problems from
+      `is_element_of` and `is_not_element_of`
+* nLab:
+  * Separation axioms: Add zaha-style diagrams?
+  * Shutt expressiveness: Create
+  * Shutt abstraction: Create
+  * meros: Create
+  * Theorems for Free!: This should be on nLab, shouldn't it?
+  * Haskell: Add links
+    https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf and
+    https://wiki.haskell.org/Hask to justify why Hask is not categorical