к
а как в коммутативных диаграммах показать что это универсальная конструкция?
Спасибо.
А как в теоркате описать ∀ и ∃ ?
Size: a a a
2021 August 13
к
в детских книжках обычно показывают продукт как коммутативная диаграмма + текстовое пояснение, что там единственный с тч до изоморфизма морфизм где-то, то есть это не совсем определение через диаграмму
ЗП
end и coend?
SK
Вот теперь понятно, спасибо)
SK
Есть какая-нибудь классическая книга, в которой про end и coend рассказывается?
NI
Например, стрелочка пунктиром и рядом значок ∃!
NI
1. MacLane, но надо думать много
2. Кванторы не так описываются, это он по мотивам хаскеля ;-)
2. Кванторы не так описываются, это он по мотивам хаскеля ;-)
NI
А так, должно быть много, где описано про концы и коконцы...
ЗП
а разве это не те интегралы?)
NI
Концы-коконцы обозначаются интегралами, да.
Но кванторы по-другому описываются.
Ты имеешь в виду другие совсем кванторы ;-)
Вот в зависимых типах уже ближе.
Если упрощённо, то кванторы, это индексированные произведение и сумма.
Навроде x пробегает элементы типа такого-то, найти произведение f(x) для всех x.
Но кванторы по-другому описываются.
Ты имеешь в виду другие совсем кванторы ;-)
Вот в зависимых типах уже ближе.
Если упрощённо, то кванторы, это индексированные произведение и сумма.
Навроде x пробегает элементы типа такого-то, найти произведение f(x) для всех x.
KV
Да что вы прикалываетесь, это просто значки из метаязыка
B
Мне, скажем, приятнее символьное читать
SK
А как кванторы описываются?
B
Это плохой способ думать о кванторах
B
Не работает на бесконечных доменах, а если разрешить так, чтобы работало, то будет формула бесконечной длины
B
Точнее, формула, которая синтаксически может развернуться в бесконечную
B
Кроме того, и в пруверах, и в голове ты бесконечность не посчитаешь
B
Семантика (модельная, но всё равно) поэтому у кванторов совсем другая, через так называемые x-варианты
B
Проще говоря, "для всех x P(x)" истинно тогда, когда не найдётся ни одного x, который не P(x) (как пример)