Ну и в базовой либе все виды должны быть

Tuple Prod Sigma Exists у нас по дизайну (синтаксические особенности базовой библиотеки)

1. Не завис, индукт
2. Не завис, пара
3. Зависим, пара
4. Зависим, индукт

Еще наличие таких примитивных штук позволяет освоить синтаксис быстрее, а также позволяет для примитивов ядра построить сигнатуры чтобы потом построить класс MLTT и туда загнать все правила-примитывы и чекнуть самим собой ядро, как в выпуске I.

Два первых примера : это интернализация MLTT (MLTT, mltt.ctt) и построение категорного групоида (PathGrpd, cat.ctt) на путях. Для этого надо прописать все синонимы для Пи Сигмы и Пути и их элиминаторов, просто чтобы читать доказательство было удобнее.

Ведь тот же вопрос можно поставить и для модуля Pi.ard 'Зачем делать синонимы для lam и app?', но там получается даже короче Pi A B вместо \Pi (x : A) -> B x. Концепцию можно сформулировать еще так: для каждого правила каждого типа MLTT свой терм и своя паблик функция!

@akuklev, подскажи как записать And /\ конекшин (contr) на Arend:

singl     (A: U) (a: A): U = (x: A) * Equ A a x
eta       (A: U) (a: A): singl A a = (a,reflect A a)
contr     (A: U) (a b: A) (p: Equ A a b): Equ (singl A a) (eta A a) (b,p) = <i> (p@i,<j>p@i/\j)

На yacctt это выглядит так:

connAnd (A : U) (a b : A) (p : Path A a b) :
 PathP (<i> Path A a (p @ i)) (<_> a) p =
 <i j> hcom 0->1 A [ (i=0) -> <k> hcom 1->0 A [ (k=0) -> <_> a, (k=1) -> p ] (p @ k)
                   , (i=1) -> <k> hcom 1->j A [ (k=0) -> <_> a, (k=1) -> p ] (p @ k)
                   , (j=0) -> <k> hcom 1->0 A [ (k=0) -> <_> a, (k=1) -> p ] (p @ k)
                   , (j=1) -> <k> hcom 1->i A [ (k=0) -> <_> a, (k=1) -> p ] (p @ k)
                   -- The diagonal is not strictly necessary, but it is cool!
                   , (i=j) -> <k> hcom 1->i A [ (k=0) -> <_> a, (k=1) -> p ] (p @ k)
                   ] a

На RedPRL так:

theorem Connection/And(#l:lvl) :
 (->
  [ty : (U #l hcom)]
  [a b : ty]
  [p : (path [_] ty a b)]
  (path [i] (path [_] ty a (@ p i)) (abs [_] a) p))
by {
 lam ty a b p =>
   abs i j =>
     `(hcom 0~>1 ty a
       [i=0 [k] (hcom 1~>0 ty (@ p k) [k=0 [_] a] [k=1 [l] (@ p l)])]
       [i=1 [k] (hcom 1~>j ty (@ p k) [k=0 [_] a] [k=1 [l] (@ p l)])]
       [j=0 [k] (hcom 1~>0 ty (@ p k) [k=0 [_] a] [k=1 [l] (@ p l)])]
       [j=1 [k] (hcom 1~>i ty (@ p k) [k=0 [_] a] [k=1 [l] (@ p l)])]
       [i=j [k] (hcom 1~>i ty (@ p k) [k=0 [_] a] [k=1 [l] (@ p l)])])
}.

\func squee (i j : I)
  => coe (\lam x => left = x) (path (\lam _ => left)) j @ i

\func upper (i j : I)
  => coe (\lam i => Path (\lam j => left = squee i j)
                         (path (\lam _ => left))
                         (path (\lam j => squee i j)))
         (path (\lam _ => path (\lam _ => left))) right @ i @ j

\func connAnd {A : \Type} {a b : A} (p : a = b) (i : I) : a = p @ i
  => path (\lam j => p @ upper i j)

\func contr (A : \Type) (a b : A) (p : Path A a b) : Path (singl A a) (theta A a) (b,p)
  => path (\lam i => (p @ i, path (\lam j => p @ upper i j)))

надо еще connOr ! :-)

squeeze маловато будет :-)

без hcom оказывается можно жить! но прямой паттерн мачинг кубов прикольнее

теоркат портируется с cubicaltt на Arend при помощи некольких регэкспов :-)

Новости по конференциям. В следующем году планирую посетить две конференции (на одну уже куплены билеты даже). Ну как конференции, в академическом мире это скорее выглядит как митап, хотя называется формально форкшопы, или по-нашему хакатоны, практические занятия, перед которыми дается лекционный интенсив.

Первая моя конференция — это Lean Forward 2019 в Амстердаме. Где я узнаю, чем дышит Lean коммюнити и расскажу им как встраивать кубическую теорию в Lean (Ground Zero github.com/groupoid/lean). Там я планирую увидеть Джереми Авигада, Руди Гринберга (который писал обзор на n2o даже как то), Кирила Коена. Организатор мероприятия — Роберт Льюис.

Вторая — это Geometry in Modal Homotopy Type Theory, которая пройдет в CMU, в Питтсбурге, где спикеры Майкл Шульман, Эгберт Райке, Урс Шрайбер. Это передний край cohesivett, и ее приложений к дифференциальной геометрии. Организатор мероприятия — Феликс Веллен, диссертация которого имеет отдельную страницу на ncatlab.

Еще я подался как спикер на fby.by, незнаю или возьмут мою тему HoTT: The Language of Space, но это единственный шанс всё же встретится с Брагилевским в 2019 году!