These are chat archives for groupoid/exe

18th
Apr 2016
Zeit Raffer
@zraffer
Apr 18 2016 06:32
ночные бдения! запись data Cut: (A: *) -> * := ... выше - я тоже это не понимаю. откуда пример? почитаем.
сам я пока прикрываю предикативную сессию и возвращаюсь к добиванию непредикативного (с ним все ясно).
Zeit Raffer
@zraffer
Apr 18 2016 06:44
по поводу viXra есть подозрение, что там псевдонаука ))
ну да, фрики
Namdak Tonpa
@5HT
Apr 18 2016 09:12
кстати по ситсемам типов меньше всего фричества, по крайней мере я ни одной статьи не нашел
мы будем первые ;-)
Он там Cut вводит в первой лекции
Вот еще новинка Proof-relevant pi-calculus http://arxiv.org/abs/1604.04575
Namdak Tonpa
@5HT
Apr 18 2016 09:17
@zraffer так а шо там с предикативной версией? почему затык?
Zeit Raffer
@zraffer
Apr 18 2016 09:29
"почему затык?" потому что затык. есть направление (описанное выше), в котором можно что-то найти, а может и нет. надо формально все выписать с 2-категориями и 2-монадами, чтобы понять, какой там уровень универсума (и еще - надо ли внутри использовать более простые кодировки, и как там у них с уровнями...). но это может занять, допустим, месяц. так что я могу сказать, что от "набросков набросков" мы перешли к просто "наброскам", вобщем я потратил неделю и лучше себе представляю "ландшафт" этой фигни. /// в то же время я могу сделать последний рывок и доделать непредикативное, вот и... доделаю.
про Cut - я все подряд эти лекции не смотрел, я там понимаю это высший индуктивный тип в хитром синтаксисе, и синтаксиса я не понимаю.
Zeit Raffer
@zraffer
Apr 18 2016 09:45
если говорить о месте, где мы находимся, то получается так - мы заканчиваем имплементацию (уровня Леан) непредикативной кодировки, и у нас на полдороги ресёрч по предикативной. причем по прагматическим причинам мы, скорее всего, выберем непредикативную в бекэнде, даже если у нас получится полностью работоспособная предикативная, из-за сложности последней.
Namdak Tonpa
@5HT
Apr 18 2016 11:18
higher-inductive-semantics.pdf
клево
да да тут как раз есть про эти truncation || A ||
который я Cut назвал
Zeit Raffer
@zraffer
Apr 18 2016 12:25
data Trunc : (A:*)->* :=
    (Mk : A -> Trunc A)
    (ForceEqu : \/(a1 a2 : A)-> Mk a1 = Mk a2)
предлагаю такой синтаксис
для такого типа, кстати, не надо выходить за рамки обычных сетоидов