Cammy/Bikeshed

From Esolang
Jump to navigation Jump to search

This page is an appendix for research done for Cammy which is too long and boring to be included on the main page.

Nomenclature

Most categorical objects are each a presentation of some wikipedia:universal property, but the current practice of mathematics does not have unambiguous symbols for most of them. Worse, most arrows do not have standard names, and sometimes not even standard titles.

The following table's rows are categorical arrows, and the columns are category theorists who have named them; each cell is a name. Our columns are:

In addition, we have three extra columns. Two are for the communities of Wikipedia and nLab respectively, and one is for Cammy.

Kerby's Category

Kerby gives a broad argument that their `i` combinator, which unquotes a single quotation and executes its stack effect, is a homomorphism. Indeed, we will imagine an entire category which routes quotations opaquely without executing them; to execute any expression in Kerby's category, simply suffix it with `i`. However, Kerby also gives a persuasive argument that lambda calculus is best understood with the identity arrow being the expression `A\A`, which corresponds precisely to `i`. We thus will use `i` for identity and reason from there.

Delta

One might expect that the usage of the Greek capital wikipedia:delta (letter) is definitely the Unicode codepoint U+0394 GREEK CAPITAL LETTER DELTA. However, Baez & Stay and Patterson use U+2206 INCREMENT, and Elliott uses U+25b3 WHITE UP-POINTING TRIANGLE. This is almost certainly a typesetting issue. The table uses U+0394 (Δ) exclusively, for screen readers.

WP nLab Cammy Curien Hagino Von Thun Kerby Baez & Stay Elliott Patterson
wikipedia:morphism#Identity [1] id id - id i id id 1
- [2] comp - - b -
wikipedia:initial and terminal objects [3] ignore 1 ! drop zap ! it I
wikipedia:product (category theory) [4] fst Fst pi1 pop k p exl -
snd Snd pi2 popd z p' exr -
pair <,> pair - c - Δ -
wikipedia:diagonal morphism [5] dup - - dup dup Δ - Δ
wikipedia:coproduct [6] left - in1 - - - inl -
right - in2 - - - inr -
case - case - - - jam -
wikipedia:monoidal category [7] assl - - - - assoc - -
assr - - - - - - -
wikipedia:free monoid [8] nil - nil [] - - - -
cons - cons cons - - - -
fold - prl fold - - - -
wikipedia:symmetric monoidal category [9] swap - - swap swap braid - σ
wikipedia:Cartesian closed category [10] curry Λ curry - - ~ curry -
uncurry - - - - - uncurry -
app App eval b - eval apply -
wikipedia:natural numbers object [11] zero - zero 0 z0 - - -
succ - succ succ - - - -
pr - pr primrec - - - -