а объект это что тогда?

Объектов вообще нет... Только стрелки

😳 ложки нет, Нео (С)

Объектов вообще нет... Только стрелки

Объект есть, ровно один (вопрос был в контексте моноидов).

Объект есть, ровно один (вопрос был в контексте моноидов).

Не, я говорю, что в теоркате объектов вообще нет

Только стрелки

Интересно

Бартош давал определение, в котором объекты были частью категории.

А категория тогда - стрелки от стрелки к стрелке?

Объекты несомненно есть, просто объект это разновидность стрелки

Объекты несомненно есть, просто объект это разновидность стрелки

Ну да, я это и имел в виду

Что объекты не нужны в аксиоматике

Как отдельная сущность

По-крайней мере мне так рассказывал математик один:)

Объекты несомненно есть, просто объект это разновидность стрелки

это как? откуда и куда?

Говорим A, подразумеваем id_A

Говорим id_A, подразумеваем A

А чо там рассказывать, на ncatlab же есть вот тут: https://ncatlab.org/nlab/show/fully+formal+ETCS

The theory of categories

то есть применительно к Хаскеллу получается (\case False -> False; True -> True) ~ (data False | True)?

не пойму какую задачу вы тут решаете...

то есть применительно к Хаскеллу получается (\case False -> False; True -> True) ~ (data False | True)?

Нет, потому что типы это не объекты

не пойму какую задачу вы тут решаете...

ничего удивительного, это же телеграм

А чо там рассказывать, на ncatlab же есть вот тут: https://ncatlab.org/nlab/show/fully+formal+ETCS

А в чем мотивация single-sorted definition of a category?

заводы стоят, одни математики кругом...

Нет, потому что типы это не объекты

а что у нас объекты?

А в чем мотивация single-sorted definition of a category?

В том чтобы можно было нормально пользоваться impredicative logic жеж

или так? (Bool -> Bool) ~ Bool?

а что у нас объекты?

Типы это подъекты жеж

подъекты?

Классы эквивалентности мономорфных стрелкок

Типы это подъекты жеж

теор кат же об убер абстракции, притянуть можно к очень многому, не?

теор кат же об убер абстракции, притянуть можно к очень многому, не?

Вообще говоря нельзя проецировать тьюринг-полные языки в теоркат :)

чето тут как-то траффика много стало

spoiler: Потому что редукция это не равенство

чето тут как-то траффика много стало

Чат вырос в полтора раза за три месяца по-моему. У вас тут нету статистик-бота?

я не добавлял

Чат вырос в полтора раза за три месяца по-моему. У вас тут нету статистик-бота?

нету 🙂

Надо бы добавить :) @combot вроде популярный

так а зачем? разве сам не замечаешь что комьюнити живое/мертвое?

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

некоторые просто любят читать статистику

особенно, когда надои ростут, сразу жить веселее становится

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

(избегать статистики любой ценой)

Ну можно в паблик её выложить. Я вот радею всей душой за коммьюнити

Надо бы добавить :) @combot вроде популярный

в описании ссыль

говорят ликвидхаскель для 8.2 сделали, для 8.0 где-то год надо было ждать

в описании ссыль

Э?

А, всё

А чо там рассказывать, на ncatlab же есть вот тут: https://ncatlab.org/nlab/show/fully+formal+ETCS

для тёмных, это авторитетный ресурс какой-то? натыкался на его упоминание в одном блоге, но не более

Ну это скорее секта, вокруг которой собираются самые долбанутые n-category theoretic и homotopy theoretic

это детище джона баэза и компании, выросло из блога https://golem.ph.utexas.edu/category/

По-моему с подачки баеза созданный

но вообще да, сейчас это точка сборки для хаеркатегорщиков

https://en.wikipedia.org/wiki/John_C._Baez

Вот эта прыщавая личность

типичный хаер категорщик

На самом деле он-то теор физик

abstraction astronomer

На самом деле он-то теор физик

корфилд из тамошних вообще философ

или так? (Bool -> Bool) ~ Bool?

Но таких стрелок 4, а булов 2, это ничего?

Но таких стрелок 4, а булов 2, это ничего?

да, не получается

а где что решают?

Но таких стрелок 4, а булов 2, это ничего?

С чего вы взяли что Bool -> Bool должен равняться Bool'у?

или так? (Bool -> Bool) ~ Bool?

Если считать Bool объектом, например, категории Set , то есть четыре стрелки Bool -> Bool. Это id, const True, const False, not. Композиция между этими стрелками - это композиция функций. И будет (id :: Bool -> Bool) ~ Bool.

Bool: Bool -> Bool Bool(x) === x

Я так это понимаю

почему newForeignPtr_ не чистая функция?

а т.к. там newIORef и можно навешивать финализаторы

то есть применительно к Хаскеллу получается (\case False -> False; True -> True) ~ (data False | True)?

так я с этого и начал

так я с этого и начал

А data это какая категория?

Я специально оговорку про Set сделал

Не все data в Set засунуть можно

я про Hask

Set — это классические множества (с классическими функциями) типа Bool = {False, True}?

сейчас мне скажут, что Hask не категория

Set - это категория малых множеств, если я правильно помню

Hask это Set с боттомами

Ну {True, False} там в любом случае есть...