Разница между параметром и аргументом

[akuklev]

Зависимые теории типов с иерархиями вселенных не позволяют говорить о вещах типа “категория всех групп”, они лишь позволяют говорить о “категориях всех U-малых групп”, проблема хорошо известная людям, занимающимся теорией категорий в теории множеств Тарского-Гротендика (ZFC + всякое множество содержится в какой-то вселенной Гротендика). Как в

Comments

[anonymous]

> А невозможность прямого переноса терма вдоль изоморфизма предотвращала парадокс Расселла.

Тогда уж парадокс Жирарда если мы говорим о теориях типов.

Кстати, по поводу

> В MLTT нет различия между параметром и аргументом.

Я пытался про это читать, но потерялся :(
Насколько я понял было несколько вариантов, самый первый из которых как раз и был подвержен парадоксу Жирарда. В итоге переделок получились экстенсиональный вариант (используется в NuPRL) и интенсиональный вариант (используется нигде?) - про какой именно из них идёт речь? И какой из них считается "каноническим"?

[akuklev]

> Насколько я понял было несколько вариантов, самый первый из которых как раз и был подвержен парадоксу Жирарда.

Да. Там было type in type. Т.е. вселенная которая сама свой элемент. Так не работает.

> В итоге переделок получились экстенсиональный вариант (используется в NuPRL) и интенсиональный вариант (используется нигде?) - про какой именно из них идёт речь? И какой из них считается "каноническим"?

Интенсиональный вариант (те или иные его расширения) используются как раз везде, кроме NuPRL/MetaPRL/RedPRL/Andromeda. В частности он используется в Agda, Coq, Idris, Lean, Arend и т.д.

[fractaler]

"она класс, а не множество"

Подскажите, пожалуйста, к кому можно поприставать по поводу того, является ли класс множеством?

[akuklev]

> Подскажите, пожалуйста, к кому можно поприставать по поводу того, является ли класс множеством

[fractaler]

Спасибо за такой обстоятельный ответ, было над чем подумать.
В разделе "§ О слове класс." при попытке найти, что такое класс ( класс - это то то и то то) пока удалось найти только как формировать класс : "классы можно формировать только из множеств".