Из комментов, про HoTT
Из комментов, цитата 1: «В смысле "когда RedPRL станет столь же удобен как ХХХ, то можно считать, что [..] применима в учебном процессе" - что здесь будет ХХХ?»
Такого XXX сейчас нет целиком, но можно собрать по частям.
Итак, вначале про Proof Assistant в отрыве от подлежащей теории:
1) Нужно максимально освободить пользователя необходимости выдумывать/выписывать строгие доказательства абсолютно очевидных вещей, для этого нужна
1а) Поддержка custom definitional ν-rules (https://arxiv.org/pdf/1304.0809.pdf).
1b) Интеграция с мощным SAT/SMT-солвером, который часть тривиальных шагов доказательства умеет сам (в F* работает, с Agda и Lean экспериментально).
1с) Поддержка тактик, как минимум как в Coq'е, только тактики должны быть современные, совместимые со всеми фичами подлежащей теории типов (в Coq сейчас тактики массово устаревшие). Но вообще ещё нужно поддержку тактик типа wlog (without loss of generality - тактики, превращающие доказательства суженного случая в полностью общие), поиска implicit conversion (как в Andromeda) и поиска implicit instance (как недавно появилось в Agda).
1d) Поддержка мощного паттерн-матчинга (в обычной математике это называется разбором случаев и доказательством по-индукции), как в Агде - разной общности в зависимости от того, удовлетворяет ли тип разбираемого выражения judgemental UIP (т.е. с тривиальным по определению равенством). Сейчас в Агде, насколько я знаю либо так, либо так. Либо для всех типов усечённый вариант, либо для всех типов наиболее общий (что несовместимо с унивалентностью).
2) Нужно максимально снизить уровень verbosity - до уровня, как уже можно писать в статьях для людей, для чего нужна мощная система implicit-аргументов и typeclass'ов.
3) Нужно дать возможность писать доказательства как люди привыкли, т.е. должна быть хорошая синтаксическая поддержка equational reasoning и monotonic reasoning, как в Lean.
4) Нужна поддержка мощной системы (first class) модулей, см. http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51
5) Нужна first-class поддержка орнаментов, чтобы была какая-то разумная реюзабельность. (Этого ещё никто не реализовал.)
6) Нужен офигенно хороший синтаксис, офигенно хороший визуальный редактор и офигенно хороший визуальный просмотрщик, где можно смотреть доказательства с динамически выбираемым пользователем уровнем подробности.
Теперь про подлежащую теорию. Во-первых, почему теория типов? Потому что мы хотим структурализма. Мы не хотим, как это описано в Бурбаках писать словами о структурах и иметь подспудно в виду, некий нетривиальный перевод на “ассемблер” теории множеств. Мы хотим сразу писать на высокоуровневом языке.
Нам нужно (а) удобство записи определений таких структур как группа, кольцо, топологическое пространство, (б) возможность вести доказательства про них на структурном уровне, (в) возможность с лёгкостью переносить доказательства вдоль изоморфизма структур, (г) возможность работать в дальнейшем с категориями групп, колец и топологических пространств.
Все эти требовария реализуются как раз в унивалентных теориях типов. Требование (г) требует как минимум наличия одной (унивалентной) вселенной. Но вообще-то с категориями хочется как-то работать, определять что такое функторы, естественные преобразования и т.д., а для этого потребна иерархия вселенных и возможность работать с полиморфными по уровню в иерархии структурами, что нам даёт теория типов под названием pCuIC (Predicative, Polymorphic, Cumulative Calculus of Inductive Constructions, к сожалению, это штуковина ещё без унивалентности), в ней реализуется Yoneda Embedding, что в других теориях типов не реализуется, насколько мне известно.
Кстати, кумулятивность вселенных и индуктивных типов тут существенна, а вот Расселовость - нет. Т.е. можно сделать теорию типов с кумулятивными вселенными Тарского (см. https://groups.google.com/forum/#!msg/homotopytypetheory/j4FooP618-Q/nSwzlkdXAQAJ).
Из комментов, цитата 2: «В стародавние времена у нас матан начинался как раз с теории множеств и ZFC. Интересно, будет-ли в будущем использоваться та же XTT в качестве базиса?»
Чтобы можно было прочитать курс матанализа не на базе теории множеств, а на базе какой-то теории типов, нам нужно чтобы эта теория типов была вычислительной, поддерживала унивалентность*, QIITs (Quotient Inductive-Inductive Types) и универсальный (непредикативный) тип утверждений Prop. Эти три ингридиента позволяют дать удовлетворительное для нужд матанализа определение вещественных чисел и пределов.
(* Унивалентность нужна для того чтобы пользоваться изоморфизмом между разными эквивалентными определения вещественных чисел.)
Вообще, именно XTT, если она действительно работает, как обещают, поддерживая при этом QIITs и Prop, хоть и не поддерживает унивалентность, в остальном прекрасна. Там верны экстенциональность для функций и унивалентность для утверждений, а то что в ней judgemental UIP и juggemental J rule - жутко удобно. Наличие QIITы ведь даёт не только вещественные числа, но и эффективные модели для любых infinitary (generalized) algebraic theories. Если она ещё и индуктивно-рекурсивные типы поддерживает и индексированные коиндуктивные типы поддерживает и кумулятивность индуктивных типов, то это вообще бомба с точки зрения широты применимости - это туда тогда вообще вся обычная математика влезать будет, кроме одного важнейшего недостатка - отсутствия возможности переносить результаты вдоль когерентного изоморфизма, то есть та самая унивалентность.
Такого XXX сейчас нет целиком, но можно собрать по частям.
Итак, вначале про Proof Assistant в отрыве от подлежащей теории:
1) Нужно максимально освободить пользователя необходимости выдумывать/выписывать строгие доказательства абсолютно очевидных вещей, для этого нужна
1а) Поддержка custom definitional ν-rules (https://arxiv.org/pdf/1304.0809.pdf).
1b) Интеграция с мощным SAT/SMT-солвером, который часть тривиальных шагов доказательства умеет сам (в F* работает, с Agda и Lean экспериментально).
1с) Поддержка тактик, как минимум как в Coq'е, только тактики должны быть современные, совместимые со всеми фичами подлежащей теории типов (в Coq сейчас тактики массово устаревшие). Но вообще ещё нужно поддержку тактик типа wlog (without loss of generality - тактики, превращающие доказательства суженного случая в полностью общие), поиска implicit conversion (как в Andromeda) и поиска implicit instance (как недавно появилось в Agda).
1d) Поддержка мощного паттерн-матчинга (в обычной математике это называется разбором случаев и доказательством по-индукции), как в Агде - разной общности в зависимости от того, удовлетворяет ли тип разбираемого выражения judgemental UIP (т.е. с тривиальным по определению равенством). Сейчас в Агде, насколько я знаю либо так, либо так. Либо для всех типов усечённый вариант, либо для всех типов наиболее общий (что несовместимо с унивалентностью).
2) Нужно максимально снизить уровень verbosity - до уровня, как уже можно писать в статьях для людей, для чего нужна мощная система implicit-аргументов и typeclass'ов.
3) Нужно дать возможность писать доказательства как люди привыкли, т.е. должна быть хорошая синтаксическая поддержка equational reasoning и monotonic reasoning, как в Lean.
4) Нужна поддержка мощной системы (first class) модулей, см. http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51
5) Нужна first-class поддержка орнаментов, чтобы была какая-то разумная реюзабельность. (Этого ещё никто не реализовал.)
6) Нужен офигенно хороший синтаксис, офигенно хороший визуальный редактор и офигенно хороший визуальный просмотрщик, где можно смотреть доказательства с динамически выбираемым пользователем уровнем подробности.
Теперь про подлежащую теорию. Во-первых, почему теория типов? Потому что мы хотим структурализма. Мы не хотим, как это описано в Бурбаках писать словами о структурах и иметь подспудно в виду, некий нетривиальный перевод на “ассемблер” теории множеств. Мы хотим сразу писать на высокоуровневом языке.
Нам нужно (а) удобство записи определений таких структур как группа, кольцо, топологическое пространство, (б) возможность вести доказательства про них на структурном уровне, (в) возможность с лёгкостью переносить доказательства вдоль изоморфизма структур, (г) возможность работать в дальнейшем с категориями групп, колец и топологических пространств.
Все эти требовария реализуются как раз в унивалентных теориях типов. Требование (г) требует как минимум наличия одной (унивалентной) вселенной. Но вообще-то с категориями хочется как-то работать, определять что такое функторы, естественные преобразования и т.д., а для этого потребна иерархия вселенных и возможность работать с полиморфными по уровню в иерархии структурами, что нам даёт теория типов под названием pCuIC (Predicative, Polymorphic, Cumulative Calculus of Inductive Constructions, к сожалению, это штуковина ещё без унивалентности), в ней реализуется Yoneda Embedding, что в других теориях типов не реализуется, насколько мне известно.
Кстати, кумулятивность вселенных и индуктивных типов тут существенна, а вот Расселовость - нет. Т.е. можно сделать теорию типов с кумулятивными вселенными Тарского (см. https://groups.google.com/forum/#!msg/homotopytypetheory/j4FooP618-Q/nSwzlkdXAQAJ).
Из комментов, цитата 2: «В стародавние времена у нас матан начинался как раз с теории множеств и ZFC. Интересно, будет-ли в будущем использоваться та же XTT в качестве базиса?»
Чтобы можно было прочитать курс матанализа не на базе теории множеств, а на базе какой-то теории типов, нам нужно чтобы эта теория типов была вычислительной, поддерживала унивалентность*, QIITs (Quotient Inductive-Inductive Types) и универсальный (непредикативный) тип утверждений Prop. Эти три ингридиента позволяют дать удовлетворительное для нужд матанализа определение вещественных чисел и пределов.
(* Унивалентность нужна для того чтобы пользоваться изоморфизмом между разными эквивалентными определения вещественных чисел.)
Вообще, именно XTT, если она действительно работает, как обещают, поддерживая при этом QIITs и Prop, хоть и не поддерживает унивалентность, в остальном прекрасна. Там верны экстенциональность для функций и унивалентность для утверждений, а то что в ней judgemental UIP и juggemental J rule - жутко удобно. Наличие QIITы ведь даёт не только вещественные числа, но и эффективные модели для любых infinitary (generalized) algebraic theories. Если она ещё и индуктивно-рекурсивные типы поддерживает и индексированные коиндуктивные типы поддерживает и кумулятивность индуктивных типов, то это вообще бомба с точки зрения широты применимости - это туда тогда вообще вся обычная математика влезать будет, кроме одного важнейшего недостатка - отсутствия возможности переносить результаты вдоль когерентного изоморфизма, то есть та самая унивалентность.