Богатой структуры там не найти, если просто пучки рассматривать в обычном смысле

У Спивака в той книжке про темпоральную теорию типов есть способ как вытянуть (po)site для определенных домейнов

Ну а пучки и на (пред)топологиях Гротендика можно офигенно "геометричных" показать ;-)

Безусловно)

Говорить, что геометрическая логика связана с какой-то геометрией, это почти то же самое, что и говорить, что топосы, это такие теории множеств ;-)

Ну, субъективное-то субъективное, но при использовании алгебраической семантики той же никаких визуальных интерпретаций в голову не придёт, поскольку алгебра не про это. В модельной семантике (стандартной) тоже не придёт, поскольку её интерпретации имеют свою собственную специфику, которую можно соотнести (и с погрешностями) разве что с семантикой в естественных языках. Теория категорий просто про некоторые абстрактные математические структуры, которые ведут себя некоторым образом. Это не даёт никакого геометрического понимания. Геометрия и топология как её подобласть далеко ушли, но, тем не менее, геометрия и топология всё же про это, как минимум в некотором смысле и как минимум за некоторыми исключениями. Так что топологическая семантика — это естественный коннект между логикой и visual / spatial thinking.

Ну, может быть, я не прав, но я всё-таки на всякий случай указал, что геометрическая логика пришла не из геометрии.

Ладно, если не нравится пример с геометрической логикой, тогда есть spatial reasoning и всякие (тоже совершенно разные, часто никак друг с другом не связанные) вещи из этого.

Приятно, что у нас в чатике появились холиворы не на тему хаскеля :)

Вопрос.

Не могу нигде найти доказательство того, что декартово произведение в Hask или в Set действительно является декартовым произведением. Ведь, там важно показать, что <f, g> будет единственным таким морфизмом, что...

Отсебятина же какая-то неубедительная получается.

Я, ведь, верно понимаю, что нужно для доказательства зафиксировать и объект-произведение, и пару проекций; и уже с учётом этого контекста доказывать единственность?

он единственный до изоморфизма же

Морфизм просто единственный

Да. И ещё. А какие есть подходы к доказательству такой единственности? В тех случаях, когда определение <f, g> не совсем прямолинейное. Мне приходится сравнивать на классах эквивалентности, у которых определение на полстраницы.

Это, вроде, про объект. А сам морфизм должен быть каноническим терминальным.

Каким терминальным?

Ну это я так сократил, что он ведёт в терминальный объект ☺️

Ну, в категории конусов. Бла-бла-бла.

Ну, очень примерно сказал. Да... ☺️

В Set всё просто доказывается.
Из свойств функции вы восстанавливаете её значения во всех точках, а значит она равна заданному по определению равенства функций в Set

Ну, то есть, по обычной схеме: возьмём h и докажем, что h = <f, g>?