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

а это откуда ?

про коннективы как аджойнты можешь почитать в Advances in Proof-Theoretic Semantics 2015ого года, раздел Categorical Harmony and Paradoxes in Proof-Theoretic Semantics

там и про кванторы тоже

с коннектив как сопряжений категорная логика в целом и началась

ловир заметил, что существование/всеобщность - левое/правое сопряжение к подстановке

Да-да

(а потом ляпнул, что логика — это раздел геометрии)

Из https://ncatlab.org/nlab/show/product+category :

This operation is the cartesian product in the 1-category Cat.

Подскажите, где можно посмотреть доказательство этого утверждения?

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

ну оно действительно несложное

👍

Просто берёшь функторы F и G, и строишь функтор F×G.

ну там так же тривиально нужно доказать про функториальность проекций и собственно универсальное свойство

"A rational person would probably ask why in axiomatic propositional calculus, one discards almost everything that one knows about logic, leaving only three axioms and one rule from which the whole edifice must be rebuilt. (That's like throwing away all of your money except for three dollars and then trying to rebuild all of your former wealth from that.) It is difficult to answer such a criticism in a rational way."

Не знаю, будет ли полезно, попотел с миграцией на новый аренд, доказал вам
https://github.com/Odomontois/Tincat/blob/master/src/Cat/Category.ard#L42

Огромное спасибо 👍

На 1.6.0.1 оно должно тайпчекаться?

Просто у меня выдаёт:

$ java -jar ~/bin/Arend.jar -L ~/src/arend/arend-lib                                                                                                                                    
[INFO] Loading library prelude
[INFO] Loaded library prelude (214ms)
[INFO] Loading library arend-lib
[INFO] Loaded library arend-lib (5543ms)
[INFO] Loading library Tincat
[WARNING] Cannot deserialize module 'Functor.Monad'
  Definition 'D' was not typechecked
  In: Functor.Monad
[INFO] Loaded library Tincat (550ms)
[ERROR] Algebra.FreeGroup:54:1: \use is not allowed on the top level
[WARNING] Functor.Monad:8:9: Definition 'precatProduct' is already imported from module Cat.Category
...
[◯] NatTrans.Iso
[◯] Universal.Product.Shuffle
[◯] Monoidal.Category
[✗] Functor.Monad
Number of modules with errors: 1
Number of modules with goals: 3
--- Done (370ms) ---

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

эта строчка у меня нормально тайпчекается