Телеграмм чат группы ru_catheory страница 135

Я нахожу всю эту позицию, что "унивалентность является теоремой" несколько странной, так как в CTT есть glueing construction, которая является унивалентностью, по сути, только в другом виде.

источник

00:17пожаловаться #11

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

У нас тоже есть похожая конструкция, из которой унивалентность следует.

источник

00:17пожаловаться #12

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

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

источник

00:20пожаловаться #13

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

Доказательство есть здесь https://github.com/JetBrains/arend-lib/blob/master/test/Equiv.ard#L434

GitHub

JetBrains/arend-lib

Contribute to JetBrains/arend-lib development by creating an account on GitHub.

источник

00:22пожаловаться #14

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

Тут не очевидно, что происходит, но, как я и сказал, всё следует из конструкции, которая у нас называется iso.

источник

00:25пожаловаться #15

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

Она является частным случаем glueing construction, если я всё правильно помню.

источник

00:26пожаловаться #16

ЕО

Евгений Омельченко in Теория категорий

По-моему это как-то так работает в CTT: на термах в нёй (включая конструкции, использующие glue и unglue) есть нормальная форма и существует алгоритм редукции к ней.
Я не прав?

источник

00:35пожаловаться #17

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

Не просто нормальная а каноническая нормальная, т.е. начинающаяся с конструктора.

источник

00:38пожаловаться #18

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

И да, есть алгоритм вычисления ее.

источник

00:38пожаловаться #19

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

У нас такого нет.

источник

00:38пожаловаться #20