Нет, mere proposition это не просто когда все элементы равны между собой, есть дополнительное условие - равенства должны быть стягиваемы.
Давайте через (x = y) обознчать тип отождествлений (type of identifications) между элементами x и y типа T. Тип T называется чистым утверждением (mere proposition) если для всяких x y : T выполняется (x = y) ≅ Unit.
Ну и заодно тип T называется множествоподобным, если для любых x y : T тип (x = y) является чистым утверждением.
Ну и заодно приведу примеры естественных не множествоподобных типов: - Тип всех конечных множеств не является множествоподобным: множество из двух элементов x := {a, b} может быть отождествлено с самим собой двумя различными способами: refl := (a => a; b => b) и swap := (a => b, b => a), таким образом тип (x = x) содержит два неравных между собой элемента refl и swap, и не изоморфен типу Unit. - Аналогично, тип всех конечных групп содержит группы, которые изоморфны сами себе более чем одним способом, и также для колец, полей и т.д. Из самих определения этих типов (это следствие аксиомы унивалентности, называемое structure identity principle) автоматически вытекает, что типы отождествлений между их элементами суть множества изоморфизмов. Если среди структур соответствующего класса существует хоть одна с нетривиальными автоморфизмами, то тип этих структур немножествоподобен.
Ну синтетический пример немножествоподобного типа вы привели сами: Синтетическая окружность 𝕊¹, задаваемая одним обычным конструктором generic-point : 𝕊¹ (точка общего положения на окружности) и одним высшим конструктором loop : (generic-point = generic-point), говорящим что кроме тривиального отождествления refl : (generic-point = generic-point) постулируется ещё дополнительное нетривиальное отождествление loop : (generic-point = generic-point) точки общего положения на окружности с самою собой. Причём т.к. постулируется оно свободно, сами собой возникают также нетривиальные отождествления loop · loop, loop · loop · loop и т.д., а также loop⁻¹, loop⁻¹ · loop⁻¹. Можно показать, что тип (generic-point = generic-point) оказывается изоморфен вовсе не Unit, а множеству целых чисел, с законом отождествления (n : Int) => loopⁿ : (generic-point = generic-point), где loop⁰ задаётся как тривиальное отождествление refl.
Однако у синтетической сферы 𝕊¹ хотя бы тип отождествлений между её элементами (точнее, между её единственным (с точностью до неразличимости) элементом “точка общего вида” generic-point и самим собой) множествоподобный. Такие типы назвают типами гомотопического уровня 1. Если у какого-то типа все типы отождествлений между элементами гомотопического уровня 1, то говорят что у него гомотопический уровень 2, и так далее.
Так вот, у синтетических сфер начиная с размерности с 2 гомотопический уровень сразу бесконечный. Там Turtles all the way down, не получается множествоподобности сколько не копай. :-)
Если что-то непонятно, обращайтесь, постараюсь подробно объяснить.
Основная проблема, как я ее вижу, не в том, что в определение 3.3.1. закралась ошибка, которую не устранили за почти 8 лет тщательной верификации текста. Исходя из этого явно ошибочного определения формально доказана Lemma 3.3.4. Every mere proposition is a set. с определением Definition 3.3.1. Hott Book эта лемма, очевидно, ложна. А из того факта, что ее "доказательство" было как-бы формально верифицировано, неизбежно следует неприятный вывод, что ложное утверждение притаилось в базовой схеме доказательств Hott Book. Это ложное утверждение позволяет доказать любое утверждение (в том числе, и ложное).
Там на словах определение неточное, а в символах верное. То что записывается в символах как
isProp(P : *) :≡ ∏ x y : P, (x = y).
на словах правильно записывается
“A type P is a mere proposition if for all x, y : P we have x = y uniformly.”
Утверждение без слова uniformly формализуется вот так:
∏ x y : P, |x = y|,
то есть что для двух любых элементов есть _какое-то_ равенство. А в определении 3.3.1 требуется, чтобы это равенство определялось однородно, там после определения есть туманный комментарий на эту тему: “Thus, to assert that “P is a mere proposition” means to exhibit an inhabitant of isProp(P), which is a dependent function connecting any two elements of P by a path. The continuity/naturality of this function implies that not only are any two elements of P equal, but P contains no higher homotopy either.”
В частности для типа 𝕊¹ мы такой функции предьявить не можем. Чтобы объяснить, почему, я сперва объясню на примере другого типа I, определяемого конструкторами lt : I, rt : I и bridge : (lt = rt). То есть с одной стороны мы про этот тип знаем, что в нем есть две точки, между которыми есть отождествление. То есть они обязаны быть неразличимы. Чтобы задать функцию на этом типе, наивно говоря достаточно было бы сказать, чему она будет равна только на конструкторе lt, ведь примени мы её к rt мы обязаны получить неотличимый результат. Но нет, гомотопическая теория типов работает не так. Чтобы задать функцию на I, нам нужно конкретно предьявить её действие на конструкторы lt, rt и bridge. Функция применённая к lt и к rt имеет полное право производить два синтаксически различных результата, скажем вещественное число с десятичным представлением 0.99999... и вещественное число с десятичным представлением 1.0000..., а вот действие этой функции на bridge - предоставляет нам отождествление 0.999... и 1.0000, в частности предоставляет доказательство того что это два синтаксических представления неразличимы как действительные числа. Но если бы тип вещественных чисел был не множествоподобным, то это было бы не просто доказательство, это был бы ещё выбор конкретного (одного из многих) способа отождествления этих двух представлений.
Вернёмся к 𝕊¹. Функция заданная на типе 𝕊¹ определяется не только своим действием на конструктор generic-point, но и своим действием на высший конструктор loop. Да, элементы generic-point и, скажем, loop • generic-point неразличимы, но задать функцию значит конкретно выписать действие на все имеющиеся конструкторы.
Попытайтесь это сделать:
f (a b : 𝕊¹) : a = b f generic-point generic-point = refl f loop generic-point = ? f generic-point loop = ? f loop loop = ?
> Утверждение без слова uniformly формализуется вот так: ∏ x y : P, |x = y|, К сожалению, я не математик (я - программист) и не знаком с терминологией и системой обозначений за рамками HottBook.
Приведенное Вами обозначение ∏ x y : P, |x = y|, как и термин uniformly в HottBook не встречается. Как я сейчас понял, вместо него в HottBook используется термин "непрерывность" для всех рассматриваемых функций в теории в том смысле, что значение функций ap(f,p) / apd(f,p) должно быть всегда единственно, но четко для не математика это нигде в книге не сформулировано. Четко говорится лишь о том, что они существуют. > В частности, для типа 𝕊¹ мы такой функции предъявить не можем. Ну задать-то ее мы можем: f(a,b: 𝕊¹) : a = b; f(generic-point, generic-point) := refl; apd(f(generic-point),loop) := loop; apd(lambda(x: 𝕊¹,f(x,generic-point),loop) := loop⁻¹; apd2(f,loop,loop) := refl; Другое дело, что, очевидно, существует бесконечное число различных способов ее определения, она не является непрерывной, и, следовательно, ее тип выходит за рамки типов функций, рассматриваемых в HottBook. Александр, большое спасибо за Ваши пояснения!
Нет, обозначение |T| встречается, только там двойные вертикальные палочки которые я не знаю как адекватно ввести с клавиатуры - это то, что назвается в книге Propositional truncation, секция 3.7.
В целом конечно хорошо бы уже перейти к второму, так сказать, изданию HoTT-Book, где бы изложение было немного более человекопригодным так сказать. Тут просто от читателя ожидается, что он одновременно и программист, свободно владеющий языками с зав.типами и математик, имеющий развитую интуицию со стороны алгебраической топологии и всё это с полуслова понимающий.
Давайте через (x = y) обознчать тип отождествлений (type of identifications) между элементами x и y типа T. Тип T называется чистым утверждением (mere proposition) если для всяких x y : T выполняется (x = y) ≅ Unit.
Ну и заодно тип T называется множествоподобным, если для любых x y : T тип (x = y) является чистым утверждением.
Ну и заодно приведу примеры естественных не множествоподобных типов:
- Тип всех конечных множеств не является множествоподобным: множество из двух элементов x := {a, b} может быть отождествлено с самим собой двумя различными способами: refl := (a => a; b => b) и swap := (a => b, b => a), таким образом тип (x = x) содержит два неравных между собой элемента refl и swap, и не изоморфен типу Unit.
- Аналогично, тип всех конечных групп содержит группы, которые изоморфны сами себе более чем одним способом, и также для колец, полей и т.д. Из самих определения этих типов (это следствие аксиомы унивалентности, называемое structure identity principle) автоматически вытекает, что типы отождествлений между их элементами суть множества изоморфизмов. Если среди структур соответствующего класса существует хоть одна с нетривиальными автоморфизмами, то тип этих структур немножествоподобен.
Ну синтетический пример немножествоподобного типа вы привели сами:
Синтетическая окружность 𝕊¹, задаваемая одним обычным конструктором generic-point : 𝕊¹ (точка общего положения на окружности) и одним высшим конструктором loop : (generic-point = generic-point), говорящим что кроме тривиального отождествления refl : (generic-point = generic-point) постулируется ещё дополнительное нетривиальное отождествление loop : (generic-point = generic-point) точки общего положения на окружности с самою собой. Причём т.к. постулируется оно свободно, сами собой возникают также нетривиальные отождествления loop · loop, loop · loop · loop и т.д., а также loop⁻¹, loop⁻¹ · loop⁻¹. Можно показать, что тип (generic-point = generic-point) оказывается изоморфен вовсе не Unit, а множеству целых чисел, с законом отождествления (n : Int) => loopⁿ : (generic-point = generic-point), где loop⁰ задаётся как тривиальное отождествление refl.
Однако у синтетической сферы 𝕊¹ хотя бы тип отождествлений между её элементами (точнее, между её единственным (с точностью до неразличимости) элементом “точка общего вида” generic-point и самим собой) множествоподобный. Такие типы назвают типами гомотопического уровня 1. Если у какого-то типа все типы отождествлений между элементами гомотопического уровня 1, то говорят что у него гомотопический уровень 2, и так далее.
Так вот, у синтетических сфер начиная с размерности с 2 гомотопический уровень сразу бесконечный. Там Turtles all the way down, не получается множествоподобности сколько не копай. :-)
Если что-то непонятно, обращайтесь, постараюсь подробно объяснить.
Reply
Да, это первое, что мне пришло в голову. Проблема в том что в определении в d Hott Book этого условия нет:
Definition 3.3.1. A type P is a mere proposition if for all x, y : P we have x = y.
Reply
Исходя из этого явно ошибочного определения формально доказана
Lemma 3.3.4. Every mere proposition is a set.
с определением Definition 3.3.1. Hott Book эта лемма, очевидно, ложна.
А из того факта, что ее "доказательство" было как-бы формально верифицировано, неизбежно следует неприятный вывод, что ложное утверждение притаилось в базовой схеме доказательств Hott Book. Это ложное утверждение позволяет доказать любое утверждение (в том числе, и ложное).
Reply
isProp(P : *) :≡ ∏ x y : P, (x = y).
на словах правильно записывается
“A type P is a mere proposition if for all x, y : P we have x = y uniformly.”
Утверждение без слова uniformly формализуется вот так:
∏ x y : P, |x = y|,
то есть что для двух любых элементов есть _какое-то_ равенство. А в определении 3.3.1 требуется, чтобы это равенство определялось однородно, там после определения есть туманный комментарий на эту тему: “Thus, to assert that “P is a mere proposition” means to exhibit an inhabitant of isProp(P), which is a dependent function connecting any two elements of P by a path. The continuity/naturality of this function implies that not only are any two elements of P equal, but P contains no higher homotopy either.”
В частности для типа 𝕊¹ мы такой функции предьявить не можем. Чтобы объяснить, почему, я сперва объясню на примере другого типа I, определяемого конструкторами lt : I, rt : I и bridge : (lt = rt). То есть с одной стороны мы про этот тип знаем, что в нем есть две точки, между которыми есть отождествление. То есть они обязаны быть неразличимы. Чтобы задать функцию на этом типе, наивно говоря достаточно было бы сказать, чему она будет равна только на конструкторе lt, ведь примени мы её к rt мы обязаны получить неотличимый результат. Но нет, гомотопическая теория типов работает не так. Чтобы задать функцию на I, нам нужно конкретно предьявить её действие на конструкторы lt, rt и bridge. Функция применённая к lt и к rt имеет полное право производить два синтаксически различных результата, скажем вещественное число с десятичным представлением 0.99999... и вещественное число с десятичным представлением 1.0000..., а вот действие этой функции на bridge - предоставляет нам отождествление 0.999... и 1.0000, в частности предоставляет доказательство того что это два синтаксических представления неразличимы как действительные числа. Но если бы тип вещественных чисел был не множествоподобным, то это было бы не просто доказательство, это был бы ещё выбор конкретного (одного из многих) способа отождествления этих двух представлений.
Вернёмся к 𝕊¹. Функция заданная на типе 𝕊¹ определяется не только своим действием на конструктор generic-point, но и своим действием на высший конструктор loop. Да, элементы generic-point и, скажем, loop • generic-point неразличимы, но задать функцию значит конкретно выписать действие на все имеющиеся конструкторы.
Попытайтесь это сделать:
f (a b : 𝕊¹) : a = b
f generic-point generic-point = refl
f loop generic-point = ?
f generic-point loop = ?
f loop loop = ?
Reply
∏ x y : P, |x = y|,
К сожалению, я не математик (я - программист) и не знаком с терминологией и системой обозначений за рамками HottBook.
Приведенное Вами обозначение ∏ x y : P, |x = y|, как и термин uniformly в HottBook не встречается.
Как я сейчас понял, вместо него в HottBook используется термин "непрерывность" для всех рассматриваемых функций в теории в том смысле, что значение функций ap(f,p) / apd(f,p) должно быть всегда единственно, но четко для не математика это нигде в книге не сформулировано. Четко говорится лишь о том, что они существуют.
> В частности, для типа 𝕊¹ мы такой функции предъявить не можем.
Ну задать-то ее мы можем:
f(a,b: 𝕊¹) : a = b;
f(generic-point, generic-point) := refl;
apd(f(generic-point),loop) := loop;
apd(lambda(x: 𝕊¹,f(x,generic-point),loop) := loop⁻¹;
apd2(f,loop,loop) := refl;
Другое дело, что, очевидно, существует бесконечное число различных способов ее определения, она не является непрерывной, и, следовательно, ее тип выходит за рамки типов функций, рассматриваемых в HottBook.
Александр, большое спасибо за Ваши пояснения!
Reply
В целом конечно хорошо бы уже перейти к второму, так сказать, изданию HoTT-Book, где бы изложение было немного более человекопригодным так сказать. Тут просто от читателя ожидается, что он одновременно и программист, свободно владеющий языками с зав.типами и математик, имеющий развитую интуицию со стороны алгебраической топологии и всё это с полуслова понимающий.
Reply
Reply
Leave a comment