мы же про потенциальные пруверы для задачника говорим

ок, приведу еще один пример, тогда)
Ники Вазу приезжала с докладом про превращение LiquidHaskell в прувер и показывала пример на LH и аналогичный (конечно же длиннее) пример на Coq, предоставленный Эндрю Аппелем. После доклада пример на Coq был переписан в полстроки))

Сетоиды аццтой! Дайошь претопосы!! ;-)

кстати, по формализациям теорката в Coq можно посмотреть пейпер, которыйя тут цитирую https://stackoverflow.com/a/40447745/2747511 и, быть может, еще одну от Амина Тимани (на гитхабе должна быть)

а теорию групп кто-нибудь формализовывал в хотт?

Вот это точно офтоп

C точки зрения теории категорий есть формальное определение что аддитивно а что мультипликативно ?

Я знаю что в линейной логике есть чёткое определение аддитивной дизюнкции и мультипликативной

Теория категорий вродибы "дружит" с этим.

Вот например КоПродукт, если соспоставить его с дизюнкцией из линейной логики то с какой ? Аддитивной или Мультипликативной ?

Группоид ведь считается мультипликативным какбы ? А малая категория это группоид с единицей

Разве что, в смысле моноидальных категорий и классической линейной логики.
Но видимо, это не то, что вы хотели.

Человек хочет универсальных определений сложения и умножения :)

Группоид считается мультипликативным потому, что композиия чего-то считается мультипликативной.

Вот например на этом nlab написано что & (аддитивную конъюнкцию) можно представить как некий оператор Case в программировании, тоесть мы имеем в наличии все объекты но только на выбор в зависимости от ситуации. В связи с этим возникает вопрос, что есть Either a b где есть Left a и Right b. Мне кажется что этом именно мультипликативная дизюнкция. Есть ли сдесь какаето путаница ? Типо это какбы сложение вариантов или чтото такое.

Если взять haskell, то там этот case оператор паттерн матчинга вообще является некомутативным паттерн матчингом. Можно ли это назвать аддитивным некомутативным оператором ?

Мы говорили о свойствах бинарных операций.
С какого боку case — бинарная операция?

Ничего там такого не написано :(

Ну аддитивная конюнкция в програмировани это что case ? на nlab ведь написано что он сопоставлен с case. Определение: все ресурсы находятся в наличии но выбрать можно только один