> ЯП со слабой типизацией - это по сути моноиды

что?

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

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

спасибо. только бестивовые и слабо-типовые — это разные вещи.

Очень хорошо, предлагаю разъяснить эту разницу в каком-то другом чате

https://youtu.be/aZjhqkD6k6w?list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&t=2838

Об этом говорил Бартош. Я просто его мысль повторил.

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

Последнее замечание. ИМХО, как я понял, он говорил, про сильную типизацию по  Хилдни-Милнеру (как в Хаскель).  А большинство слабо-типизированных языков по Хилдни-Милнеру имеют один тип. А их собственные типы - это надстройка, придуманная разрабочиками компилятора.

можно пример такого языка с надстроенными типами?

ОК. Юрий, постараюсь поресерчить  и ответить в другом чате (наверно по Haskell) попозже.

или я сам пересмотрю Бартоша

ХМ - как лямбда-исчисление, только про 2 операции: абстракцию и применение. В любых практичных языках есть ещё набор базовых типов, как константы в лямбда-исчислении. ХМ - о том, как из любых заранее заданных базовых типов делать более развесистые.

Здравствуйте. Я человек далёкий от высоких материй. Мой основной вопрос как из эпиморфизма в ТК следует что функция surjective в сетах. Смотрю https://youtu.be/O2lZkr-aAqk?t=2540 и пытаюсь понять как он из surjective function на сетах выводит определению эпиморфизма в ТК.  Его рассуждение основывается на том, что есть такие функции g1 и g2 в сет С, которые отличаются только для точек вне image функции f из сета A в B. Но ведь эпиморфизм (и surhective) это свойство функции(морфизма), а не сета(категории), эти "отличающиеся"   g1 g2 так и останутся определенными,  если мы поменяем f так что она станет surjective, все рассуждение разваливается .

@yamlcoder Это же просто доказательство от противного. Предположим, f не сюръекция, тогда можно подобрать g1, g2, такие, что g1 o f = g2 o f, но не g1 = g2, а это противоречит исходному предположению об эпиморфности f. Ну значит сюръекция

Вот это и не могу понять. Наличие g1 и g2 из B в C никак не зависит от наличию/отсутствия сета A и какой то там функции f из A в B. g1 и g2 просто есть

Черт поймешь как оно работает

Так и не должно зависеть. Условие эпиморфности говорит: для любых g1, g2 бла-бла. А мы нашли такие g1 и g2, для которых не бла-бла, в этом противоречие

Перечитал, кажется что-то щелкнуло, буду смотреть в окно на дождь и думать дальше

Он же там в принципе и обьясняет, что в понятии функции участвуют элементы, о которых в категории ничего не известно. Доказывать свойства можно только с помощью композиции морфизмов и получаются определения немного вывернутыми. Вместо существует элемент идет утверждение для любых морфизмов.

Кирилл мне тут лучше и проще объяснил :)