Ну, синтаксические модели шире всё-таки. Но из конструктивистских соображений точно.

отсутствие каноничности /= отсутствие пруф ассистента

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

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

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

я не говорю про не/тотальность, я говорю про не/каноничность, тотальность не портится добавлением аксиом

Хм, пойду всё-таки почитаю про каноничность

Ага, прочитал. Аксиомы не вычисляются, но не считаются нормальными формами, и тем самым разрушают каноничность.

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

ну так нет, мы просто останавливаем вычисление и всё

Очень странное сравнение

Появился такой вопрос:
Обозначим за Norm категорию нормированных векторных пространств.
В качестве объектов нормированные пространства.
В качестве морфизмов линейные отображения сохраняющие норму.
Если даны два нормированных пространства (V1,n1) и (V2,n2)
(Нормы n1:V1 -> R,n2:V2 -> R),то
линейное отображение f : V1 -> V2,такое,что :
Для любого вектора v из V1:
n1(v) = n2(f(v2)),то
f будет морфизмом в данной категории.
Тогда как будет выглядеть копроизведение семейства объектов в этой категории?

Прямая сумма с нормой в виде суммы норм не подходит?

Для конечных хотя бы

Я попробовал,не выходит.
Если берём для 2-х пространств
(V1,n1) и (V2,n2).
h1 : V1 -> V1 x V2
h2 : V2 -> V1 x V2
- стандартные вложения в
(V1 x V2,n1 + n2).

Пусть дано пространство (W,s),а также морфизмы
z1 : V1 -> W
z2 : V2 -> W

Один из вариантов построения нужного морфизма:
f : V1 x V2 -> W
f((v1,v2)) = z1(v1) + z2(v2) - линейное отображение.
Но сохранит ли оно норму?
n1+n2((v1,v2)) = n1(v1) + n2(v2) =
s(z1(v1)) + s(z2(v2))
,Но в общем случае
s(f((v1,v2))) = s(z1(v1) + z2(v2))
≠ s(z1(v1)) + s(z2(v2))

Т.е. необходимо свойство
s(x+y) = s(x) + s(y).
Возможно я как-то не так все строю или где-то тут ошибка.

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

Я думаю, что и здесь просто нет кодекартовости

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

Какие (хорошие? не факт, нужно уточнить) книги есть по ТК:

1. Bartosz Milewski's, Category Theory for Programmers — очень простая и понятная, даже для программистов. Но после неё всё равно не можешь понимать почти ничего из других книг, имхо :)

2. Mac Lane, Categories for the Working Mathematician — судя по описанию в чате: хорошая, строгая. Но может быть сложно, если ты не математик.

3. Steve Awodey, Category Theory — судя по описанию в чате: тоже неплохая, проще Маклейна. Но некоторые не смогли осилить даже её — видимо, не такая простая. Во вступлении говорится, что книга "для не математиков" в дополнение к книге Маклейна.

4. Robert Goldblatt, Topoi: The Categorial Analysis of Logic — судя по описанию в чате: кому-то кажется намного проще, чем Маклейн, и больше понравилась. Кому-то чем-то сильно не понравилась, но без подробностей. Кажется, что критикующий в итоге стал к ней относится нейтрально.

5. Peter Smith, Category Theory: A Gentle Introduction — мало информации. Кто-то хвалил — для программистов просто и понятно.

6. David Spivak, Category Theory for the Sciences — писали, что много ругают. Но отзывов в чате немного.

7. "Неплохой учебник по теоркату: https://drive.google.com/file/d/1G4wierA0s8VC6qs3PbHnC5vXH32Fv--6" с сайте с материалами (в закрепе). Автор "george66 с dxdy". Кто-то хвалит, кто-то говорит, что книга ужасна — и сложно и непонятно. Но отзывов в чате не много.

8. Benjamin C. Pierce, Basic Category Theory for Computer Scientists — кажется, что книга достаточно простая. Но отзывов в чате, вроде, не было.

9. Brendan Fong, David Spivak — Seven Sketches in Compositionality: An Invitation to Applied Category Theory. 
Несколько раз хвалили в чате. Критики пока не видно.

Есть ещё Steven Roman, Harold Simmons и другие. Но по ним мало информации.

Вопрос к коллективному разуму: если у вас есть мнение относительно одной или нескольких вышеуказанных (или неуказанных) книг — черканите пару слов, пожалуйста. Может быть получится собрать больше разноплановых отзывов. И новичкам потом будет легче ориентироваться — когда и что лучше читать, какие у какой книги плюсы и минусы.

Спасибо!

Я бы семь скетчей как минимум добавил в список

А можно, плиз, ссылку?
А то упоминания в чате видел, а где книга (или статьи) не знаю