(Untitled)

[jtootf]

добрый день

в данный момент пытаюсь разобраться в ТК, читая книгу "Goldblatt. Topoi: The Categorial Analysis of Logic" (так уж получилось, что у меня есть только англоязычный её вариант), в процессе разбора возникают вопросы. буду благодарен, если поможете разобраться

Comments

[antilamer]

Пример: Группа целых чисел со сложением.

Объект - неважно какой, назовем его N.
Морфизмы: По одному морфизму на каждое целое число. Целому числу k сопоставим морфизм, который назовем M(k).
Единичный морфизм: id(N)=M(0)
Композиция морфизмов: M(a).M(b) = M(a+b)
Каждая стрелка - изо, т.к.: M(k).M(-k)=M(0)=id(N).

[jtootf]

а какая связь между N и k?

[antilamer]

Никакой.

Категория задается тройкой (граф G, id :: ob G -> ar G, (.) :: ar G -> ar G -> ar G).
Зададим категорию, соответствующую группе целых чисел со сложением:
(G, id, (.))
где граф G = {
узлы: ровно один узел, который я назову Foo - его название не имеет никакого значения, да и сам он сам по себе никакого значения не имеет - просто чтобы было откуда куда проводить стрелки :)
стрелки: по одной стрелке из Foo в Foo для каждого целого числа. Стрелку, соответствующую целому числу k, я назову M(k).
}
функция id = M(0)
функция (.) M(a) M(b) = M(a+b).

[jtootf]

ага. кажется, начало доходить, спасибо

[antilamer]

Да, еще конечно для задания категории надо доказать левую и правую единичность единичных стрелок во всех объектах (в нашем случае объект всего один) и ассоциативность (.)

Не помню, ты Coq умеешь читать? Может, на Coq написать, чтобы совсем не было неоднозначностей?

[jtootf]

Coq, увы, даже не смотрел; кое-какое знакомство из подобных языков есть только с Epigram

[antilamer]

Ну тогда может кому-то еще будет интересно :)

Record Category : Type := mkCat

[jtootf]

в принципе даже читаемо, хотя без знания Coq трудно :(

к слову, в чём существенные различия между Coq, Agda, Epigram? цели у них у всех вроде более-менее общие

[antilamer]

Не знаю, я только Coq умею :)

[nponeccop]

Agda2 читабельнее и писабельнее