These are chat archives for groupoid/exe

17th
Apr 2016
Zeit Raffer
@zraffer
Apr 17 2016 06:44
массивненько! но мы вроде конкатенативными заниматься не собирались же?
Namdak Tonpa
@5HT
Apr 17 2016 15:47
не, не собирались
nponeccop
@nponeccop
Apr 17 2016 16:29
В любом случае надо закончить начатое
Namdak Tonpa
@5HT
Apr 17 2016 19:18
ну это просто я как новости отрасли запостил
я лично по аппликативным языкам угораю
Namdak Tonpa
@5HT
Apr 17 2016 19:58
вот еще новости отрасли http://arxiv.org/pdf/1604.03799v1.pdf
Namdak Tonpa
@5HT
Apr 17 2016 20:06
я начитался про групоиды и хочу HIT, Path и вот это все )
прочитал книгу Applied Elementary Topology Хирста
и думаю найти какие-то прикладные задачи алгебраической топологии которые можно было решить с помощью EXE
Namdak Tonpa
@5HT
Apr 17 2016 20:42
у нас в языке EXE нехватает конструкции with
для того чтобы точки индуктивных конструкторов связывать
Namdak Tonpa
@5HT
Apr 17 2016 21:01
и еще мне интересно как записть в EXE тип I с двумя конструкторами L и R, но которые не выколотые точки как у Bool true и false, а связаные между собой, что-то типа инвариантного функторв L -> R и R -> L
Namdak Tonpa
@5HT
Apr 17 2016 21:09
    record Groupoid: * :=
           ([*]: Path a b -> Path b c -> Path c a)
           (inv: Path a b -> Path b a)
           (id: Path a a)
Namdak Tonpa
@5HT
Apr 17 2016 21:14
еще хотел задать вопрос по этому типу:
 data Cut: (A: *) -> * :=
      (inhabit A)
      (trunc: Cut A -> Cut A -> I)
   with
        trunc a b L => a
        trunc a b R => b
типа такого наверно
data I: * :=
       (L: R -> I)
       (R: L -> I)
вообщем непонятно
Namdak Tonpa
@5HT
Apr 17 2016 21:24
по группоидам типа эта статья считается первой
venedig-2.ps
The groupoid interpretation of Type Theory. Hoffman & Streicher 1996
тут тоже интересные абстракты http://hott-uf.gforge.inria.fr/complete_HoTTUF15.pdf
nponeccop
@nponeccop
Apr 17 2016 21:30
я тут фрикоархив нашел http://vixra.org/setlog/
Namdak Tonpa
@5HT
Apr 17 2016 21:31
пиздец люди плодовитые
судя по тому что пишут
в соотвествии с космическим кубом
то всего должно быть 8 флейворов гомотопических теорий
вот я хочу увидеть эти восемь групоидов )
Namdak Tonpa
@5HT
Apr 17 2016 21:54
немного непонятно про J и K операторы
в статье Хоффмана и Страйхера
idpeel — это что то для пропозиционного равенства типа наших Equ которые мы уже написали?
нашел про idpeel еще в книге по MLTT http://www.cse.chalmers.se/~bengt/papers/hlcs.pdf
Namdak Tonpa
@5HT
Apr 17 2016 22:05
Там типа чтобы Uniqueness of Identity Proof доказать надо еще K элиминатор
Namdak Tonpa
@5HT
Apr 17 2016 22:37
блумберг жжот https://github.com/bloomberg/bucklescript
nponeccop
@nponeccop
Apr 17 2016 22:44
http://vixra.org/author/florentin_smarandache чувак 800 пейперов написал