Думаю какую аватарку на новый канал запилить, пока кроме ПΣ ничего на ум не приходит

Может у вас будут более яркие идеи!

Приехали видосики с f(cafe). HoTT: The Language of Space в полном метре (3 часа). https://www.youtube.com/watch?v=giwrTkgGH10&list=PLGMl-uAnnXVXCLSnGy-c4hSQGFc65OoFj

пытаюсь записать Абелеву Категорию. Итак, формальное определение, начнем пока с аддитивной категории, как прекурсору к предабелевой :-). Аддитивная категория — это категория, в которой: 1) hom имеет структуру abgroup (должна быть инстанциация этого рекорда, т.е. категориальная конструкция); 2) должен быть 0-объект (z0), такой, что для любого объекта А, 0 -> A -> 0 (zer), 0-объект является терминалом и котерминалом [битерминалом]; 3) существуют продакты (mul,pi1,pi2) и копродакты (sum,inl,inr)[бипродакты]; 4) работает закон коммутативности относительно категорной композиции и групповой операции.

abcategory: U
 = (X: U) -- group
 * (hom: X -> X -> U) -- abgroup
 * (id: (x: X) -> hom x x)
 * (c: (x y z: X) -> hom x y -> hom y z -> hom x z)
 * (homSet: (x y: X) -> isSet (hom x y))
 * (left1: (x y: X) (f: hom x y) -> Path (hom x y) (c x x y (id x) f) f)
 * (right1: (x y: X) (f: hom x y) -> Path (hom x y) (c x y y f (id y)) f)
 * (assoc: (x y z w: X) (f: hom x y) (g: hom y z) (h: hom z w)
   -> Path (hom x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h)))
 * (z0: X)
 * (zer: (x: X) -> (z: X) * (l: hom z x) * (r: hom x z) * Path X z z0)
 * (mul: X -> X -> X)
 * (sum: X -> X -> X)
 * (pi1: (A B: X) -> hom (mul A B) A)
 * (pi2: (A B: X) -> hom (mul A B) B)
 * (inl: (A B: X) -> hom A (sum A B))
 * (inr: (A B: X) -> hom B (sum A B))
-- f: Hom B C = abgroup, g, h: Hom A B = abgroup
-- f o (g + h) = f o g + f o h
-- f, g: Hom B C = abgroup, h: Hom A B = abgroup
-- (f + g) o h = f o h + g o h
--  * (left: (A B C: X) (f: hom B C) (g h: hom A B) -> Path (hom A C) (c A B C f (..))
 * U

zer — место для доказательства контрактабильности 0-объектов (up to iso)
mul, sum — продакты и копродакты (по аналогии с топосом, CCC)
осталось записать условия

f o (g + h) = f o g + f o h, (f + g) o h = f o h + g o h, где + — операция группы

и не понятно как экспозить abgroup в качестве гомоморфизма, видимо уже в имплементации, надо выбрать юнит гроуп какую-то.

unitAbGroup: abgroup
 = ((unit,setUnit),(((op,asso,id,(lx,rx)),inv,(li,ri)),comm)) where
   op: unit -> unit -> unit = \(x y: unit) -> y
   id: unit = tt
   inv: unit -> unit = \(x: unit) -> x
   lx: (x: unit) -> Path unit (op id x) x = \(x: unit) -> <i>(op id x)
   rx: (x: unit) -> Path unit (op x id) x = undefined
   li: (x: unit) -> Path unit (op (inv x) x) id = undefined
   ri: (x: unit) -> Path unit (op x (inv x)) id = undefined
   asso: isAssociative unit op = undefined
   comm: isCommutative unit op = undefined

Единичная Аддитивная Категория

instance: abcategory = (Ob,Hom,id,c,homSet,L,R,Q,e,zer,mul,sum,pi1,pi2,inl,inr,Ob) where
   Ob: U = unit
   Hom (x y: Ob): U = abgroup
   id (x: Ob): Hom x x = unitAbGroup
   e: Ob = tt
   c (x y z: Ob) (f g: abgroup): abgroup = unitAbGroup
   homSet (x y: Ob): isSet (abgroup) = undefined
   L (x y: Ob) (f: abgroup): Path (abgroup) (c x x y (id x) f) f = undefined
   R (x y: Ob) (f: abgroup): Path (abgroup) (c x y y f (id y)) f = undefined
   Q (x y z w: Ob) (f g h: abgroup):
     Path (abgroup) (c x z w (c x y z f g) h)
                    (c x y w f (c y z w g h)) = undefined
   zer: (x: Ob) -> (z: Ob) * (l: Hom z x) * (r: Hom x z) * Path Ob z e = undefined
   mul: Ob -> Ob -> Ob = \(x y: Ob) -> tt
   sum: Ob -> Ob -> Ob = \(x y: Ob) -> tt
   pi1: (x y: Ob) -> Hom (mul x y) x = \(x y: Ob) -> unitAbGroup
   pi2: (x y: Ob) -> Hom (mul x y) y = \(x y: Ob) -> unitAbGroup
   inl: (x y: Ob) -> Hom x (mul x y) = \(x y: Ob) -> unitAbGroup
   inr: (x y: Ob) -> Hom y (mul x y) = \(x y: Ob) -> unitAbGroup

Собрал тестовую версию диссертации, получилось 70 страниц всего (половина объема). До нового года планирую докинуть текста до 120 страниц и допереводить с английского на украинский.

Кому интересно полистать — пермалинк https://github.com/groupoid/groupoid.space/blob/master/tex/dissertation/manuscript/diss.pdf

@akuklev Привет, меня попросили написать обзор на Arend, на него уже можно нашу базовую либу Групоид Инфинити портировать? :-)

Привет. Точно не уверен, но думаю что можно. 😊

Ребята, ну что, кто хочет попробовать на кубике от ДжетБрейнс пописать? Гарантирую, что вы будете первые! Портируем нашу либу!

$ git clone https://github.com/JetBrains/Arend && cd Arend
$ ./gradlew
$ ./gradlew jarDep
$ git clone https://github.com/JetBrains/arend-lib
$ java -jar ./build/libs/arend.jar -s arend-lib/src

Базовая либа Аренд компилица SUCCESSFULLY

Кубик надо полагать Харперовский, Картезиан Кубикал Тайп Теори (coe)

Arend Library — 175K
Groupoid Infinity — 504K

можно работать!

ты имеешь ввиду просто по порядку https://github.com/groupoid/infinity/tree/master/priv это брать и писать на Арене?

Ну почему по-порядку, то что интереснее :-)

https://github.com/groupoid/infinity/blob/master/arend/Proto.ard#L38 ­— хм, есть же встроенные пары \Sigma, в чём смысл писать свои? У таких пар даже синтаксис вспомогательный есть, pair.1 и pair.2

Так это ж нон депендент