Лёг спать, стал думать о топосах - задавал уже вопрос в bacat, а чё, всякий well-pointed topos is Boolean? (это у меня подозрение такое закралось). Дык. Только доказал (ну там два байта переслать, точнее, две точки сложить), пошел вниз к лаптопу, пошукал на интернетах - а уже пару дней назад ктото на нкатлабе это дело написал. Ну только что я добавил там к статье, что Set тут не пришей не пристегни, в любом элементарном топосе имеет место.
Следующий вопрос более коварный. А что, вот есть топос с таким свойством, что всякая монада в нём апликативна. Из этого часом не следует, что он well-pointed? Небось, очевидно. Обратно-то известный факт, Моджи ещё при Брежневе писал.
Если так, то знаете что? Тогда весь ваш Хаскель булев до мозга костей. И надо чинить. Потому что на булевость надеяться не надо. Не надо.
П.С. Ещё у меня тачпад онемел, ничего не чует; приволок с работы мышь и вожу ею по дивану. Хорошая мышь, майкрософтовская, с колёсиком.
Следующий вопрос более коварный. А что, вот есть топос с таким свойством, что всякая монада в нём апликативна. Из этого часом не следует, что он well-pointed? Небось, очевидно. Обратно-то известный факт, Моджи ещё при Брежневе писал.
Если так, то знаете что? Тогда весь ваш Хаскель булев до мозга костей. И надо чинить. Потому что на булевость надеяться не надо. Не надо.
П.С. Ещё у меня тачпад онемел, ничего не чует; приволок с работы мышь и вожу ею по дивану. Хорошая мышь, майкрософтовская, с колёсиком.