[CS][λ] Интересные развития исчисления.

2-категория получается из 1-категории введением дополнительных ограничений на совокупность стрелок.

Нет.

Если говорить о теоркате в рамках теории множеств - да.

Можно популярнее?

Изначально

Пофигу, что там было изначально.

потом ее методы... Если у вас результаты...

Давайте не будем передёргивать. Во-первых, между методами теории и её результатами есть разница. Во-вторых, что более важно, методы гомологической алгебры давно уже вышли за пределы алгебраической топологии.

Если говорить о категориях, которые можно задать в рамках ZFC

Нам ведь не надо обязательно в ZF.

То есть в рамках теории категорий такое понятие как «категория» сформулировать нельзя, я верно понял ваше утверждение?

Неверно.

Потому что если можно - это неминуемо будет стрелкой.

Не будет.

Потому что в теоркате _нету_, вообще _нету_ никаких объектов кроме стрелок.

Есть стрелки. Есть объекты. Есть категории. Есть 2-категории. Всё это - разные вещи.

> А следовательно, зависеть от неё что-либо не может. QED.

Да с чего вы взяли то? Вот истинность вашего утверждения f: forall a. a -> a => f x = x, как я уже неоднократно говорил, от семантики зависит. Если мы возьмем семантику типизированного лямбда-исчисления с полиморфизмом - утверждение истинно. Возьмем другую (например с возможностью рантайм-диспатча по типам и соответствующего правила типизации) - не будет.

Если мы возьмем семантику типизированного лямбда-исчисления с полиморфизмом - утверждение истинно.

Угу. Точнее так: если мы будем рассматривать его в типизированной лямбде с полиморфизмом. Операционная семантика идёт лесом.

> Неверно.

Тогда получаем очевидное противоречие.

Не будет.

А чем еще оно может быть, если в теории не задается ничего кроме стрелок?

Есть стрелки. Есть объекты. Есть категории. Есть 2-категории. Всё это - разные вещи.

Нет, еще раз. У вас в принципе пропозициональные переменные не могут принимать никакого значения кроме как стрелки (то как для ZFC forall x: x - множество, в теоркате forall x: x - стрелка, стрелка - эта такая штука, которую может пробегать x и которая удовлетворяет ряду аксиом). И теория формулируется для стрелок. Есть стрелки - и все, больше ничего кроме стрелок. объекты, категории, 2-категории - это все частные случаи стрелок. Ну, например, объект - это id-стрелка, категория - это, соответственно, id-стрелка в Cat и т.д.

> Угу. Точнее так: если мы будем рассматривать его в типизированной лямбде с полиморфизмом. Операционная семантика идёт лесом.

Если пустить семантику лесом, то тогда это НЕ будет типизированным лямбда-исчислением с полиморфизмом. т.к. пока мы не задали семантику - это не типизированное лямбда-исчисление с полиморфизмом, а какая-то НЕХ. Так что пока мы не задали семантику (а сказать «мы работает в рамках типизированного лямбда-исчисления с полиморфизмом» - это задание семантики в том числе) об истинности вашего утверждения говорить нлеьзя.

> Можно популярнее?

Если определить категорию, как алгебраическую структуру в рамках теории множеств, а не задавать в виде собственной формальной теории, добавляя набор аксиом к ЛПП.

Пофигу

Вам - пофигу, мне - нет.

Давайте не будем передёргивать.

К, не будем. Если мы начали использовать методы теории групп где-то еще, то теория групп не перестает быть теорией групп. И алгеброй.

А чем еще оно может быть, если в теории не задается ничего кроме стрелок?

Из ложной посылки можно вывести что угодно.

У вас в принципе пропозициональные переменные не могут принимать никакого значения кроме как стрелки

Неверно.

объекты, категории, 2-категории - это все частные случаи стрелок.

Нет.

объект - это id-стрелка

Нет, конечно, что за чушь. Есть объекты и есть id-стрелки. Между ними есть естественная биекция, но это разные вещи.

Если вы из всей теории категорий выучили только альтернативную формулировку, которой давным-давно никто не пользуется и которую придумали только для выпендрёжа, то почитайте что-нибудь нормальное.

Если пустить семантику лесом

Этого я не предлагал. Я предлагал пустить лесом ОПЕРАЦИОННУЮ семантику.

Если определить категорию, как алгебраическую структуру в рамках теории множеств, а не задавать в виде собственной формальной теории, добавляя набор аксиом к ЛПП.

Что значит «ЛПП»?

У теории категорий есть независимая аксиоматика, но она не получается «добавлением аксиом» к чему бы то ни было.

Блин, опять поторопился. Сорри.

Вам - пофигу, мне - нет.

Да это ваши проблемы, и только ваши. Математика - не философия, в ней исторические факты значения не имеют.

Если мы начали использовать методы теории групп где-то еще, то теория групп не перестает быть теорией групп. И алгеброй.

Нет, конечно. Но это означает, что мы вышли за пределы теории групп.

> Что значит «ЛПП»?

Логика первого порядка.

Неверно.

Верно.

Нет.

Да.

Нет, конечно, что за чушь. Есть объекты и есть id-стрелки. Между ними есть естественная биекция, но это разные вещи.

Нет. В аксиоматике есть совокупность стрелок и dom/cod, которые каждой стрелке сопоставляют соответствующую id-стрелку. объектов не вводится, они используются чисто для удобства.

Этого я не предлагал. Я предлагал пустить лесом ОПЕРАЦИОННУЮ семантику.

Но если вы не задали операционную семантику - вы не задали свое исчисление.

> Да это ваши проблемы, и только ваши.

То же могу сказать и вам.

Математика - не философия, в ней исторические факты значения не имеют.

Считать ли некий раздел подразделом другого раздела или нет - это не математический факт.

Нет, конечно.

То есть для теории групп - нет, а для теории гомологий - да? Так?

Верно.

Нет, увы. Вы просто не знаете практически ничего из теории категорий. Вот и мелете чушь.

В аксиоматике есть совокупность стрелок и dom/cod, которые каждой стрелке сопоставляют соответствующую id-стрелку. объектов не вводится, они используются чисто для удобства.

Вы выучили одну, никем реально не используемую, систему аксиом категории. Заметим, ОДНОЙ КАТЕГОРИИ, а не ТЕОРИИ КАТЕГОРИЙ.

Но если вы не задали операционную семантику - вы не задали свое исчисление.

Почему же? Я могу задать другую семантику.

То же могу сказать и вам.

Ошибаетесь. «Пофигу» - это не проблема.

Считать ли некий раздел подразделом другого раздела или нет - это не математический факт.

Безусловно. Но и исторические факты к этому отношения не имеют.

То есть для теории групп - нет, а для теории гомологий - да? Так?

Нет. Если мы используем методы алгебраической топологии где-то ещё, мы выходим из алгебраической топологии. И вы, что ожидаемо, не заметили более важного пункта: методы гомологической алгебры уже давно не имеют никакого отношения к топологии.

> Нет, увы.

Увы, да.

систему аксиом категории

Я и не говорил нигде об аксиоматике ОДНОЙ КАТЕГОРИИ.

Почему же? Я могу задать другую семантику.

И тогда это будет _другое_ исчисление.

> Безусловно. Но и исторические факты к этому отношения не имеют.

И какие же имеют?

Увы, да.

Ещё раз. Вы выучили маленький кусочек теорката. Почему-то вы считаете, что на этом всё заканчивается. Ошибаетесь.

Я и не говорил нигде об аксиоматике ОДНОЙ КАТЕГОРИИ.

Вы только о ней и говорили. Причём об аксиоматике, отличающейся от той, которая в настоящее время повсеместно используется.

И тогда это будет _другое_ исчисление.

Отнюдь. «Другую» - в смысле «не операционную». Денотационную, например. Её достаточно, чтобы задать исчисление.

И какие же имеют?

Состояние науки в настоящий момент, очевидно.

> Причём об аксиоматике, отличающейся от той, которая в настоящее время повсеместно используется.

Ну так вы могли бы давным-давно привести ссылку на нее, вместо того, чтобы заниматься пустой болтологией.

Отнюдь. «Другую» - в смысле «не операционную». Денотационную, например. Её достаточно, чтобы задать исчисление.

С денотационной вы свое утверждение не докажете.

> Состояние науки в настоящий момент, очевидно.

Это только ваше субъективное мнение. Как и тот факт, что состояние науки - субъективный критерий.

Ну так вы могли бы давным-давно привести ссылку на нее, вместо того, чтобы заниматься пустой болтологией.

Забанили в гугле?

http://en.wikipedia.org/wiki/Category_(mathematics)#Definition

С денотационной вы свое утверждение не докажете.

Я и не буду. Фил Вадлер это уже сделал (см. знаменитую статью «Theorems for free!»).

Это только ваше субъективное мнение.

Да нет, это просто осознание того, что «раздел A является подразделом раздела B» - утверждение, зависящее от времени.

Не надо пытаться запихнуть гомологическую алгебру в топологию. Не влезет. Гомологической алгеброй занимаются алгебраисты, на кафедрах высшей алгебры, в алгебраических журналах, применяя чисто алгебраические методы.

> Забанили в гугле?

http://en.wikipedia.org/wiki/Category_(mathematics)#Definition

Это что это вы мне тут суете? Это же самое старое классическое определение категории в рамках теории множества, как алгебраической структуры, оно даже не общее по всем n-категориям, да и неполно, т.к. категории, в которых объекты и hom-множества не образуют класс, не описывает. Мало того, без теории множеств вы вообще не можете развивать теоркат на базе этого определения, т.к. в нем не постулируется, вообще говоря, существования какой-бы то ни было категории. То есть без теории множеств мы _не можем_ построить ни одной категории. Вы таки приведете ссылку на вашу «новую аксиоматику которой все пользуются» или нет?

Я и не буду. Фил Вадлер это уже сделал (см. знаменитую статью «Theorems for free!»).

С чего вы взяли, что он это сделал без операционной семантики?

Не надо пытаться запихнуть гомологическую алгебру в топологию.

Зачем мне его пихать, если он и так там?

банальный пример - в рамках подобного определения вы не сможете описать даже категорию Set, т.к. Obj_Set - не класс.

Это что это вы мне тут суете?

Аксиомы категории.

в рамках теории множеств

По крайней мере, не в рамках ZF.

оно даже не общее по всем n-категориям

Естественно, так как 2-категория - это НЕ категория, это нечто большее.

Вы таки приведете ссылку на вашу «новую аксиоматику которой все пользуются» или нет?

Сюрприз. Все пользуются старой.

Нет, есть, конечно, аксиоматически независимое построение теорката, но оно пока что работает как proof of concept, не более.

С чего вы взяли, что он это сделал без операционной семантики?

С того, что я читал статью.

Зачем мне его пихать, если он и так там?

То есть, прочее вы предпочли проигнорировать?

Obj_Set - не класс.

Как раз-таки класс. Самый большой, какой бывает.

> С того, что я читал статью.

Ну тогда вы должны знать, что без использования операционной семантики у него бы доказать ничего не вышло.

Сюрприз. Все пользуются старой.

Сюрприз! Мы говорили об аксиоматическом построении теорката, хрен ли вы лезете в разговор тогда, если даже не понимаете о чем речь? Предоставьте мне ссылку на аксиоматическое построение теорката, где есть стрелки/ктегории/n-категории блаблабла, которое вы обещали, или вы просто бестолковое трепло, которое лезет в предмет, ни бельмесав нем не смысля.

Естественно, так как 2-категория - это НЕ категория, это нечто большее.

Если 2-категория - это НЕ категория, то существуют некие категорные свойства, которым 2-категория не удовлетворяет. Каким? Если же что-то удовлетворяет всем категорным свойствам, то это что-то - категория. Кроме того, это в вашем устаревшем определении есть разница между 2-категорией и категорией, в общем случае категория определяется совокупностью стрелок с ограничениями, причем все n-стрелки лежат _в той же самой_ совокупности. Насовать их туда или нет - это дело нашего вкуса, хотим категория с n-стрелками - суем. Далее, чтобы эта категория стала n-категорией, нам надо просто добавить ряд ограничений на эти стрелки.

Ну тогда вы должны знать, что без использования операционной семантики у него бы доказать ничего не вышло.

Я знаю, что операционной семантикой он не пользовался. Он пользовался одним из вариантов денотационной. Ваше «бы» мне не интересно, это теоретизирование (без аргументов), а я вижу практику.

Мы говорили об аксиоматическом построении теорката

Да ну? По-моему, вы говорили о превосходстве теормножа перед теоркатом.

которое вы обещали

Не обещал.

Если 2-категория - это НЕ категория, то существуют некие категорные свойства, которым 2-категория не удовлетворяет. Каким?

1-категория состоит из двух совокупностей (объекты и морфизмы). 2-категория - из трёх.

это в вашем устаревшем определении

Я хотя бы привожу определения. Вы неспособны даже на это.

в общем случае категория определяется совокупностью стрелок с ограничениями, причем все n-стрелки лежат _в той же самой_ совокупности.

Ссылку, пожалуйста. На сколько-нибудь авторитетный источник.

хотим категория с n-стрелками - суем.

Ну-ну. Математика, к вашему сведению, не позволяет просто «хотим - суём», это вы не в ту степь заехали.

> Я знаю, что операционной семантикой он не пользовался.

А я знаю, что пользовался.

Да ну?

Ну да.

По-моему, вы говорили о превосходстве теормножа перед теоркатом.

Во-первых - не говорил, во-вторых - везде подразумевался теоркат, как отдельная формальная система. И это не только явно подразумевалось из контекста, но и было сказано открытым текстом.

Не обещал.

То есть вы не можете привести ссылку на аксиоматику с категориями, объектами и т.д.? я так и думал. Обычное трепло.

1-категория состоит из двух совокупностей (объекты и морфизмы). 2-категория - из трёх.

Вы, видимо, плохо прочитали вопрос? Я спросил - какому категорному свойству _не удовлетворяет_ 2-категория. Я не вижу нигде в определении категории требования, что там нет других совокупностей кроме объектов и стрелок. Они не постулируется - но их существования не запрещается. как я уже упоминал - в определении вообще существования категории не постулируется, следуя вашей логики категорий нет вообще.

Ссылку, пожалуйста. На сколько-нибудь авторитетный источник.

Ба, так вы, получается, даже банальную Categories for the Working Mathematician не осилили! Чего же вы тогда лезете со свиным-то рылом, да в калашный ряд? В этом контексте считаю разговор с вами бессмысленным. Извольте поднять свой уровень знаний - тогда и продолжим.

> следуя вашей логики категорий нет вообще.

Поясню - в определении категории не сказано, что в категории существует хотя бы один объект. Так же как не сказано, что существуют другие совокупности кроме объектов и hom-множеств. Нет второго - нет и первого.

А я знаю, что пользовался.

Процитируйте соответствующее место.

везде подразумевался теоркат, как отдельная формальная система.

Это достаточно бессмысленное утверждение. Если мы используем категорный язык, нам всё равно, используем мы отдельную аксиоматизацию теорката, или же строим его на основе чего-то.

То есть вы не можете привести ссылку на аксиоматику с категориями, объектами и т.д.?

Во-первых, могу, и не на одну. Во-вторых, это не имеет отношения к теме разговора.

Я спросил - какому категорному свойству _не удовлетворяет_ 2-категория.

Она не удовлетворяет свойству «состоять из двух совокупностей». Она состоит из трёх.

Я не вижу нигде в определении категории требования, что там нет других совокупностей кроме объектов и стрелок.

Прочитайте внимательно. Ту же википедию, например. Там прямо написано: «category consists of...» и далее - из чего она consists.

даже банальную Categories for the Working Mathematician не осилили

Не наглейте, эта книга к банальным не относится. Разумеется, я её читал, и прекрасно помню, что там сказано. Сказано там следующее (пересказываю своими словами - если нужна точная цитата, то подождите, пока я доберусь до дома): так как единичные морфизмы взаимно-однозначно соответствуют объектам, формально можно определить категорию при помощи одних лишь морфизмов. Однако, определение там таки приведено через объекты. Попробуйте прочесть чуть дальше первого раздела.

в определении категории не сказано, что в категории существует хотя бы один объект.

Да, и существует категория, в которой объектов нет. И что?

не сказано, что существуют другие совокупности кроме объектов и hom-множеств

Сказано, см. выше.

> Прочитайте внимательно. Ту же википедию, например. Там прямо написано: «category consists of...» и далее - из чего она consists.

в 2-категории объекты есть? есть. стрелки есть? есть. значит свойство «consist of...» выполняется.

Во-первых, могу

Ну так давайте.

Во-вторых, это не имеет отношения к теме разговора.

С каких пор тема разговора не относится к теме разговора?

Она не удовлетворяет свойству «состоять из двух совокупностей».

В указанном определении не сказано, что категория должна состоять _только_ из двух совокупностей. Там сказано, что _среди прочих_ совокупностей эти две должны быть.

так как единичные морфизмы взаимно-однозначно соответствуют объектам, формально можно определить категорию при помощи одних лишь морфизмов.

Речь вообще шла про n-категории, что вы уже радостно забыли.

Да, и существует категория, в которой объектов нет. И что?

Вы не поняли. Не используя теорию множеств, мы и не можем рассматривать никакую категорию кроме пустой вообще. Мы просто не можем доказать существование какой-либо категории кроме пустой. Потому что у нас нету ни одной аксиомы, которая бы позволила нам это сделать. В рамках подобного определения (на базе теории множеств) у нас нету вообще никакого способа ввести категорию, кроме как задать класс (в соответствии с теоретико-множественной аксиоматикой) и потом доказать, что поверх этого класса можно задать структуру категории, удовлетворяющую заданным требованиям. То есть, если мы пользуемся подобным определением, то работать внутри теорката, не выходя за его пределы в теорию множеств мы просто не можем.

в 2-категории объекты есть? есть. стрелки есть? есть. значит свойство «consist of...» выполняется.

Нет, не выполняется. 2-категория не СОСТОИТ из объектов и морфизмов, там есть ещё и 2-морфизмы.

В указанном определении не сказано, что категория должна состоять _только_ из двух совокупностей.

Глагол «состоит из», как и английский «consists of», означает именно это, если нет дополнительных оговорок.

_среди прочих_

Это ваши фантазии. Там нет никаких «прочих».

Речь вообще шла про n-категории, что вы уже радостно забыли.

Лжёте, речь шла об определении категории. А не n-категории.

Не используя теорию множеств, мы и не можем рассматривать никакую категорию кроме пустой вообще.

Ну и что?

Потому что у нас нету ни одной аксиомы, которая бы позволила нам это сделать.

Где? В определении категории - да. Так это определение и не претендует на что-то большее, нежели определение того, что такое категория. Если вы возьмёте независимую аксиоматизацию - вы увидите там, как минимум, постулированное требование существования категории с одним объектом и одним морфизмом. Но, опять-таки: и что?

То есть, если мы пользуемся подобным определением, то работать внутри теорката, не выходя за его пределы в теорию множеств мы просто не можем.

Почему не можем? Теормнож нужен при таком подходе для того, чтобы заложить некие основы, а вся настоящая работа идёт в теоркатегоре. Или вы считаете, что работать на джаве нельзя, не используя машинные коды?

> Нет, не выполняется. 2-категория не СОСТОИТ из объектов и морфизмов, там есть ещё и 2-морфизмы.

Определение категории не запрещает категории кроме объектов и морфизмов иметь 2-морфизмы, 3-морфизмы и любую другую НЕХ. Определение требует существования объектов, морфизмом и того, чтобы удовлетворялись аксиомы. Но не требует не-существования чего-либо другого.

Глагол «состоит из», как и английский «consists of», означает именно это, если нет дополнительных оговорок.

Конечно же, нет. То, о чем говорите вы, это оборот «состоит из и только из». Это математика, а не естественный язык, в конец концов. И на самом деле за вашими «consist of» стоят высказывания теории множеств.

Это ваши фантазии. Там нет никаких «прочих».

Ваша фантазия - это то, что кто-то запрещает категории иметь доп. структуру. Вот этого там точно нет.

Лжёте, речь шла об определении категории. А не n-категории.

Нет, перечитайте пост.

Почему не можем?

Вы сами ответили, почему.

Определение категории не запрещает категории кроме объектов и морфизмов иметь 2-морфизмы, 3-морфизмы и любую другую НЕХ.

В сад. Любое определение однозначно описывает определяемый объект, без всяких НЁХ.

Это математика, а не естественный язык, в конец концов.

В математике - ещё более. В естественном языке подобная вольность ещё допустима.

Ваша фантазия - это то, что кто-то запрещает категории иметь доп. структуру.

Никто не запрещает, только не надо говорит, что это осталось категорией. Это категория с дополнительной структурой, не являющиеся частным случаем категорий. Так же, как кольца не являются частным случаем групп, например.

Нет, перечитайте пост.

Блин, если вы приводите книжку МакЛейна в качестве авторитетного источника, то это автоматически означает, что про n-категории вы забыли вообще. У него там n-категории только в каком-то примечании к 2-категориям, причём ни для тех, ни для других формального определения нет, а то, что есть явно различает объекты, морфизмы и 2-морфизмы.

Вы сами ответили, почему.

Я вам объяснил, почему работать в теоркате можно, даже не вспоминая о теории множеств.

> В сад. Любое определение однозначно описывает определяемый объект, без всяких НЁХ.

Ну да. И 2-категория - однозначно удовлетворяет определению категории.

В математике - ещё более. В естественном языке подобная вольность ещё допустима.

Я про что и говорю. В естественном языке вы еще можете написать «consist of ...» и тут могут быть разночтения (хотя на деле никаких разночтений не бывает, т.к. это стандартный в математике оборот и обозначает он именно то, что я сказал), в строгом определении же у вас там нету никаких условий на отсутствие у категории доп. структуры.

Это категория с дополнительной структурой, не являющиеся частным случаем категорий.

Вы уже сами заговорились. Так «это категория» или «это не категория»? И, еще раз - если это _категория_ то укажите чему из категорного определения 2-категория не управляет (напоминаю - существование Obj, существование Hom, существование композиции на Hom (еще открытый вопрос что такое в данном случае композиция) и выполнение свойств для композиции). Никаких утверждений, постулирующих _несуществование_ чего-либо в определении нет.

Так же, как кольца не являются частным случаем групп, например.

Конечно же, является. Определению группы кольцо удовлетворяет? Да.

Блин, если вы приводите книжку МакЛейна в качестве авторитетного источника, то это автоматически означает, что про n-категории вы забыли вообще. У него там n-категории только в каком-то примечании к 2-категориям, причём ни для тех, ни для других формального определения нет, а то, что есть явно различает объекты, морфизмы и 2-морфизмы.

в моем издании - 12.5

> в моем издании - 12.5

Там n-категория определяется как совокупность стрелок + n «согласованных» упорядоченных категорных структур. убирая/добавляя структуры - меняем «уровень» категории, стрелки не трогаем при этом. Это, кстати, логично - объекты ничего к категории не добавляют, то есть вся информация о категории хранится в стрелках максимального «уровня». Стрелки нижнего уровня мы можем восстановить из стрелок более высокого при помощи соответствующей структуры.

И 2-категория - однозначно удовлетворяет определению категории.

Нет. 2-категория добавляет всякую НЁХ, она же - 2-морфизмы.

в строгом определении же у вас там нету никаких условий на отсутствие у категории доп. структуры.

Ещё раз. Категория - это не категория с допструктурой. Это разные вещи.

укажите чему из категорного определения 2-категория не управляет

Тому, что категория должна СОСТОЯТЬ ИЗ двух совокупностей (не ВКЛЮЧАТЬ или СОДЕРЖАТЬ две совокупности, а СОСТОЯТЬ ИЗ).

Определению группы кольцо удовлетворяет? Да.

Нет. Для этого надо убрать одну бинарную и одну 0-арную операцию. Учите основы.

Там n-категория определяется как совокупность стрелок

Ещё раз. У МакЛейна формально не определяется даже 2-категория. Про n-категорию у него только маленькое примечание. И даже если расшифровать это примечание и довести до полного определения, из него сразу получится, что n- и (n+1)-категории - разные вещи, не являющиеся частными случаями друг друга.

> Нет. 2-категория добавляет всякую НЁХ, она же - 2-морфизмы.

Ну да, добавляет. Но в определении категории не сказано, что всякую НЕХ добавлять нельзя. От того, что мы к категории добавили НЕХ, категория не перестает удовлетворять определению. И категорией быть не перестает.

Ещё раз. Категория - это не категория с допструктурой. Это разные вещи.

Категория - это не категория. От оно! От до чего дошли!

Тому, что категория должна СОСТОЯТЬ ИЗ двух совокупностей (не ВКЛЮЧАТЬ или СОДЕРЖАТЬ две совокупности, а СОСТОЯТЬ ИЗ).

Пожалуйте мне формализацию понятия «состоять из ...». Иначе этот спор беспредметен.

Нет. Для этого надо убрать одну бинарную и одну 0-арную операцию. Учите основы.

Кольцо удовлетворяет аксиомам групп и без того, чтобы убирать те или иные операции. Вообще, то, чем вы занимаетесь, банальнейшая софистика. Кольцо не является группой точно в том же самом смысле, в котором группой не является группа, определенная через другую аксиоматику. Например, можно задать свойства нейтрального элемента через нульарную операцию, а можно просто через существование удовлетворяющего определенному набору свойств элемента. В первом случае нульарная операция есть - а во втором нет. И, по-вашему, группа по первому определению не будет являться группой по-второму. Ведь они «состоят из» разных элементов!

Ещё раз. У МакЛейна формально не определяется даже 2-категория. Про n-категорию у него только маленькое примечание.

«Гляжу в книгу - вижу фигу». У него сперва идет формальное определение 2-категории, потом альтернативное определение и потом определения n-категории и w-категории. Я вам даже уже пальцем ткнул, где смотреть.

> И даже если расшифровать это примечание и довести до полного определения, из него сразу получится, что n- и (n+1)-категории - разные вещи, не являющиеся частными случаями друг друга.

Из него сразу получится, что n+1-категория получается добавлением к n-категории одного элемента к упорядоченному набору категорных структур. то есть формально строго n+1-категория частный случай n-категории. Или вы под понятием «частный случай» понимаете нечто свое, не то, чт понимают под этим все математики.

Ещё раз про то что язык ТК «эквивалентен» теоретико-множественному? Вычислительно эквивалентен с точки зрения теории рекурсивных функций? А то есть сколько угодно разных вычислительно эквивалентных языков. Осталось только выяснить какой из них более высокоуровневый.

Вот в Categories for the practising physicist автор позиционирует категорную формулировку КМ как высокоуровневое её представление, при этом все остальные формулировки, получается, уровнем ниже. А все остальные это теоретико-множественные (как у Дирака — некоммутативные алгебры).

Или другой пример — изучение ADT. Есть сколько угодно тезисов и статей про data fusion оптимизации которые (тезисы и статьи) используют категорный язык, ванильную теорию множеств при этом никто не использует. Модель ADT как категории позволяет использовать разные мощные инструменты работающие в рамках ТК — мы сразу получаем фреймворк для работы с рекурсивными и полиморфными ADT (полиморфизм — простая квантификация по объектам категории), данные и ко-данные как сопряжённые функторы (т.е. определение ко-типа выводится из определения типа), фреймворк для generic программирования — возможность по виду ADT (т.е. по заданию категории) строить все те основные функции которые работают с этим ADT (разные функторы — общего вида, аппликативные, «забывающие» и так далее). Ну и фреймворк для data fusion с использованием F-алгебр.

И как это всё будет выглядеть классически, без ТК? Размеченные объединения декартовых произведений? А дальше?

Вы всегда можете перевести любое утверждение туда-обратно.

Только вы этого не можете. Чисто технически. Как вы будете пероводить сопряжённые функторы или F-алгебры из категорных моделей? Как универсальные алгебры специального вида? Но так никто не делает. А даже если и сделать — вы просто построите себе подобие теории категорий для удобства изложения.

Смотря что вы собираетесь понимать под языком.

В данном случае — типы и правила для типов, синтаксис языка и его семантику.

Аналогично в теоркате - мы не строим модель языка, мы просто определяем разные категории с определенными свойствами.

Нет. Тут единственное число — одна 2-категория это одна модель одного языка (что понимается под «языком» — выше), т.е. именно что модель. А вот одним множеством никакой модели мы не задаём.

Мне кажется, вы не читаете, что я пишу. Я же просто попросил привести конкретную теорему и ее перевод на термины предметной области.

Ну я же привёл ключевые слова — coherence, monoidal category, Church-Rosser. Или вы хотите чтобы я копипастил теоремы из публикаций — вне их контекста это не имеет никаго смысла.

Я же там специально пояснил — подразумевалось, что она нигде кроме логики и топологии не используется иначе чем «переформулируем то, что уже есть».

Ну вот всё вот это это развитие или перевод? Правда, в квантовой физике сейчас всё настолько туманно, что хороший перевод тоже может стать развитием :) Но даже если и перевод — суть в том, что существенно разные разделы переведены на один язык и при этом появляются нетривиальные аналогии между разделами (т.е. между логикой, топологией, теорией вычислений и физикой).

Просмотрел ваши посты - не нашел. Может, еще раз кинете?

Про LC в виде 2-категории? Тут и ссылки на другие статьи там же.

> Осталось только выяснить какой из них более высокоуровневый.

Да ни какой из них не более «высокоуровневый». Все зависит от того, какие объекты надо описывать.

Только вы этого не можете. Чисто технически.

«Чисто технически» любое категорное утверждение - это и так теоретико-множественное утверждение. И его вообще не надо переводить.

Нет. Тут единственное число — одна 2-категория это одна модель одного языка (что понимается под «языком» — выше), т.е. именно что модель. А вот одним множеством никакой модели мы не задаём.

Задаем набором множеств. Причем _тем же самым_, что самое забавное. Просто в теоркате мы взяли и этот набор обозвали «2-категорией».

Ну я же привёл ключевые слова — coherence, monoidal category, Church-Rosser.

Да при чем тут ключевые слова? Дайте конкретную теорему и ее перевод. Это несколько строчек текста. Чего вы словоблудием занимаетесь? Хотя я понимаю, чего - теорем-то таких нет. Вот и приводить в пример - нечего.

Ну вот всё вот это это развитие или перевод?

Это вообще на данный момент _ничего_. В смысле теоркат ради самого теорката.

Но даже если и перевод — суть в том, что существенно разные разделы переведены на один язык и при этом появляются нетривиальные аналогии между разделами (т.е. между логикой, топологией, теорией вычислений и физикой).

Вы не поверите - эти разделы _изначально_ были изложены на одном языке. И нетривиальные аналогии _сперва_ появляются в рамках какой-либо предметной области и только _потом_ описываются в рамках теорката. Когда они уже есть.

Но в определении категории не сказано, что всякую НЕХ добавлять нельзя.

Определение однозначно описывает определяемый объект.

Категория - это не категория.

Не надо передёргивать. Милостивый государь - не государь.

Пожалуйте мне формализацию понятия «состоять из ...».

Учите русский язык.

Кольцо удовлетворяет аксиомам групп и без того, чтобы убирать те или иные операции.

Нет. Группа - это четвёрка «множество, умножение, единичный элемент, обращение». Кольцо - это шестёрка «множество, сложение, ноль, умножение, единица, обращение по сложению».

Кольцо не является группой точно в том же самом смысле, в котором группой не является группа, определенная через другую аксиоматику.

Да. Но между ними есть простое взаимно-однозначное соответствие, которое позволяет, допуская вольность речи, говорить, что это одно и то же.

Между 2-категориями и 1-категориями нет взаимно-однозначного соответствия. Даже инъекции из 2-категорий в 1-категории нет. Есть простая инъекция обратно, так что, допуская вольность речи (опять) можно утверждать, что 1-категория есть частный случай 2-категории. Обратно - не вольность речи, а ошибка.

У него сперва идет формальное определение 2-категории

Вообще-то, нет. У него есть нечто, примерно похожее. То, что легче довести до определения.

И там есть объекты, морфизмы и 2-морфизмы.

потом определения n-категории

Нет. У него есть, опять-таки, нечто, что можно, приложив определённые усилия, превратить в определение.

И, опять же, 3-категория и 4-категория будут сугубо разными вещами при этом.

то есть формально строго n+1-категория частный случай n-категории.

Нет. Опять-таки: различные n+1-категории могут при этом получится из одной и той же n-категории. Так что не получится даже с вольностью речи.

К слову, на счет необходимости типов для задания нетипизированного лямбда-исчисления. У вас объекты - типы, термы - стрелки, редукции - 2-стрелки. Вы можете взять в качестве объектов теперь стрелки, в качестве стрелок - 2-стрелки, в результате получаете категорию, которая эффективно содержит всю структуру вашей первоначальной 2-категории. Типы - не нужны.

> Определение однозначно описывает определяемый объект.

Как это противоречит моему утверждению?

Не надо передёргивать. Милостивый государь - не государь.

А четное число - не число. Непрерывная функция - не функция. моноидальная категория - не категория. Пустое множество - не множество. Непустое множество, кстати, тоже не множество. Отсюда сразу следует вывод - т.к. любое множество либо пусто либо нет, то любое множество - не множество. А значит, множеств не существует. Только что мы с вами доказали противоречивость ZF.

Да. Но между ними есть простое взаимно-однозначное соответствие, которое позволяет, допуская вольность речи, говорить, что это одно и то же.

А с чего вы взяли, что должно быть взаимо-однозначное соответствие?

можно утверждать, что 1-категория есть частный случай 2-категории.

Как раз нельзя. Мы можем с 2-категорией делать то, чего не можем с 1-категорией. Так что 2-категория не есть частный случай 1-категории. А вот обратное верно. Все, что мы можем делать с 1-категорией верно и для 2-категории. Все свойства, все теоремы 1-категорий верны для 2-категорий, так же как все свойства групп выполняются для колец.

Вообще-то, нет.

Вообще-то - да. Идите и прочитайте уже.

И там есть объекты, морфизмы и 2-морфизмы.

Там - есть. а в определении, которое идет следом, эти совокупности уже не разделяются.

Нет. У него есть, опять-таки, нечто, что можно, приложив определённые усилия, превратить в определение.

Там дано формально строгое определение. n-категория - совокупность стрелок с упорядоченным набором категорных структур, удовлетворяющих определенным свойствам. Чем это определение вас не устраивает? Дайте альтернативное, в конце концов.

И, опять же, 3-категория и 4-категория будут сугубо разными вещами при этом.

4-категория получится из 3-категории добавлением одной структуры, так что 4-категория будет частным случаем 3-категории.

Как это противоречит моему утверждению?

Вы пытаетесь добавить к определяемому объекту то, чего в определении нет.

А четное число - не число.

Опять-таки, не надо передёргивать.

А с чего вы взяли, что должно быть взаимо-однозначное соответствие?

Оно там просто есть. При чём тут «должно быть»? Если его не будет, то подобная вольность речи станет недопустимой.

Как раз нельзя.

Как раз можно, ибо 1-категории канонически вкладываются в 2-категории.

Так что 2-категория не есть частный случай 1-категории.

Наконец-то, дошло. Именно это я столько времени и объясняю.

Идите и прочитайте уже.

Читал, неоднократно. Приводите цитату. С одной вы уже облажались, теперь посмотрим на вторую.

4-категория получится из 3-категории добавлением одной структуры, так что 4-категория будет частным случаем 3-категории.

Снова-здорово. 3-категории канонически вкладываются в 4-категории, так что их можно считать «частным случаем» последних. Обратное неверно.

> Вы пытаетесь добавить к определяемому объекту то, чего в определении нет.

И дальше что?

Опять-таки, не надо передёргивать.

Где я передергиваю? По определению, 2-категория - это 1-категория для которой выполняется блаблабла. Четное число - это число, для которого выплняется блаблабла. В чем разница?

Оно там просто есть. При чём тут «должно быть»?

Перефразирую. С чего вы взяли, что взаимо-однозначное соответствие необходимо для того, чтобы допускать подобную вольность речи?

ибо 1-категории канонически вкладываются в 2-категории.

Ну да. За счет этого любая 2-категория - частный случай 1-категории, но не наоборот.

Наконец-то, дошло.

Тьфу, опечатка. Там 1 и 2 поменять местами.

Приводите цитату. С одной вы уже облажались

про цитаты пока что только вы облажались, когда аксиоматику теорката привести не смогли.

Читал, неоднократно. Приводите цитату.

я, вобщем-то, уже и привел. n-категория - «множество X (ну у Маклейна везде множества вместо классов) с n различными категорными структурами (#_i, s_i, t_i) для i = 0,..., n-1, которые коммутируют между собой, а каждая единица структуры i есть единица структур j: j > i». И чуть выше дана строгая формализация того, что значит «коммутируют между собой».

> Снова-здорово. 3-категории канонически вкладываются в 4-категории, так что их можно считать «частным случаем» последних. Обратное неверно.

Что это за бред? Все наоборот. X - частный случай Y, если для Х верны все свойства Y, то есть если в любом утверждении, где фигурирует Y, мы можем поставить X и получить верное утверждение. Если у нас есть истинное высказывание f(Y), где Y - 1-категория, то оно верно и для f(X), где X - 2-категория. По-этому 2-категория - частный случай 1-категории. С другой стороны, обратную замену мы сделать можем не всегда, т.к. некоторые высказывания о 2-категориях для 1-категорий вообще не имеют смысла (высказывания о 2-стрелках).

> И чуть выше дана строгая формализация того, что значит «коммутируют между собой».

И что значит «категорная структура».

Кстати, а как по-вашему (с выделением n-стрелок в отдельные классы по n) определяется w-категория?

И дальше что?

И вот.

По определению, 2-категория - это 1-категория для которой выполняется блаблабла.

Чушь. По определению, 2-категория - это 1-категория ПЛЮС ДОПОЛНИТЕЛЬНАЯ СТРУКТУРА. Не ОГРАНИЧЕНИЯ, а ДОПСТРУКТУРА.

С чего вы взяли, что взаимо-однозначное соответствие необходимо для того, чтобы допускать подобную вольность речи?

С того, что иначе вас перестанут понимать. Если вы будете отождествлять объекты, между которыми нет канонического взаимно-однозначного соответствия, вас не поймут. Именно поэтому, в частности, если R - некое кольцо, то говорят не «группа G изоморфна R», а «группа G изоморфна аддитивной группе R».

Там 1 и 2 поменять местами.

Тогда неверно.

про цитаты пока что только вы облажались

Напоминаю. Мы говорили о статье Вадлера «Theorems for free!» Вы сказали откровенную чушь, после чего просьбу привести цитату аккуратно замолчали.

«множество X (ну у Маклейна везде множества вместо классов) с n различными категорными структурами

Ну да, я про это и говорю. Любой квалифицированный математик способен сделать из этого чёткое определение (правда, опять-таки отличающееся от общепринятого - см. википедию). А теперь скажите, правда ли, что по-вашему „множество с двумя структурами“ - частный случай „множества с одной структурой“? Или будем дискутировать о том, что „одна“ якобы значит на самом деле „хотя бы одна“?

> А теперь скажите, правда ли, что по-вашему «множество с двумя структурами» - частный случай «множества с одной структурой»?

Естественно. Чуть выше я описал, что понимается под «X есть частный случай Y». Наш случай (добавление структуры) как раз подходит.

> С того, что иначе вас перестанут понимать.

Для понимания в данном случае достаточно зафиксировать некоторое каноническое вложение. Группы - в аддитивную группу кольца, 1-категорию - в 1-категорию, образованную стиранием лишней структуры с 2-категории, ну и т.д.