В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

Аренда физических серверов любых конфигураций под любые запросы - 1С бухгалтерия, игровые сервера, нагруженные проекты, интернет-магазины!

qwarta.ru подробнее

Size: a a a

Теория категорий

569 membersпожаловаться на группу
2020 February 06

Oℕ

Oleg ℕizhnik in Теория категорий
Gymmasssorla
Можно ведь сделать композицию двух композиций Bool -> Bool и получить четвёртый морфизм  Bool -> Bool
Вы опять путаете типы с термами
источник
23:42пожаловаться#1

Oℕ

Oleg ℕizhnik in Теория категорий
Композиция не обязательно порождает что-то новое.
Например композиция const True и const False даст const True тот же, что вы взяли
источник
23:50пожаловаться#2

O

Orbarax in Теория категорий
Oleg ℕizhnik
Ну в общем, мне кажется трудно переплюнуть теоркат в стремлении всё обобщить, включая себя, в особенности себя.
Так что обвинить в "почему никто не придумал что-то более общее" именно теоркат вряд ли получится.
HoTT?
источник
23:50пожаловаться#3

Oℕ

Oleg ℕizhnik in Теория категорий
И четвёртый неупомянутый морфизм из Bool -> Bool нельзя получить как композицию упомянутых трёх (иначе Эмиль Пост очень расстроится)
источник
23:51пожаловаться#4
2020 February 07

МБ

Михаил Бахтерев in Теория категорий
Orbarax
HoTT?
Это частный случай, когда все категории являются группоидами.
источник
08:41пожаловаться#5

Oℕ

Oleg ℕizhnik in Теория категорий
Михаил Бахтерев
Это частный случай, когда все категории являются группоидами.
Не все являются
источник
08:42пожаловаться#6

Oℕ

Oleg ℕizhnik in Теория категорий
классический HoTT выражается на языке (∞, 1)- категории, т.е.один уровень не изоморфизмов - собственно функции, есть
источник
08:44пожаловаться#7

Oℕ

Oleg ℕizhnik in Теория категорий
А уже равенства на каком-то типе представляют из себя ∞- группоид
источник
08:46пожаловаться#8

МБ

Михаил Бахтерев in Теория категорий
Oleg ℕizhnik
Не все являются
Ну, да... Плохо выразился. Но, смысл в том, что HoTT не обобщает категории, а моделируется некоторыми их частными случаями.
источник
08:48пожаловаться#9

МБ

Михаил Бахтерев in Теория категорий
P.S. А что-то в памяти застряло, что HoTT - это 2-группоид. Пойду погуглю, чего это такое.
источник
08:49пожаловаться#10

МБ

Михаил Бахтерев in Теория категорий
Оу. А в рунете исследования группоидов весьма популярны. Не ожидал
источник
08:50пожаловаться#11

МБ

Михаил Бахтерев in Теория категорий
https://www.maths.ed.ac.uk/~tl/cambridge_ct14/cambridge_ct14_talk.pdf - об интеграле Лебега на языке категорий
источник
09:04пожаловаться#12

V

Valery in Теория категорий
Михаил Бахтерев
Ну, да... Плохо выразился. Но, смысл в том, что HoTT не обобщает категории, а моделируется некоторыми их частными случаями.
HoTT  сама является теорией, описывающей oo-категории. Не все oo-категории можно так описать, но довольно много. Конкретно, все конечно полные.
источник
12:11пожаловаться#13

МБ

Михаил Бахтерев in Теория категорий
Valery
HoTT  сама является теорией, описывающей oo-категории. Не все oo-категории можно так описать, но довольно много. Конкретно, все конечно полные.
Да, но понятие категории, тем не менее, hott не обобщает
источник
12:23пожаловаться#14

NI

Nick Ivanych in Теория категорий
Valery
HoTT  сама является теорией, описывающей oo-категории. Не все oo-категории можно так описать, но довольно много. Конкретно, все конечно полные.
Имеется в виду итерированное обогащение или интернализация?
Точнее, (∞,1)-обогащение и (∞,1)-интернализация.
источник
12:39пожаловаться#15

V

Valery in Теория категорий
Nick Ivanych
Имеется в виду итерированное обогащение или интернализация?
Точнее, (∞,1)-обогащение и (∞,1)-интернализация.
Скорее последнее, но если говорить точно, то просто категория моделей HoTT является моделью oo-категории определенных oo-категорий. Абсолютно аналогично категориям с расслоениями или модельным категориям.
источник
12:42пожаловаться#16

NI

Nick Ivanych in Теория категорий
Михаил Бахтерев
Да, но понятие категории, тем не менее, hott не обобщает
Как вот тут чууть выше сказано, (∞,1)-категории несут за собой ещё и парочку способов описания (∞,n)-категорий.
источник
12:51пожаловаться#17

Oℕ

Oleg ℕizhnik in Теория категорий
Nick Ivanych
Как вот тут чууть выше сказано, (∞,1)-категории несут за собой ещё и парочку способов описания (∞,n)-категорий.
Ну я думаю, что Михаил очень категорично воспринял понятие обобщения, буквально как инъекцию понятий.
В этом смысле действительно простая категория не является гомотопической теорией типов, а значит HoTT - не обобщение понятия категории
источник
12:54пожаловаться#18

Oℕ

Oleg ℕizhnik in Теория категорий
Т.е. HoTT может служить языком, на котором обобщить можно, но сам по себе не является обобщением
источник
12:55пожаловаться#19

МБ

Михаил Бахтерев in Теория категорий
Ну, да... Тонкостей много
источник
12:57пожаловаться#20