Всем привет. Хочу поделиться своим опытом использования библиотеки ProvingGround, написанной на Скале с использованием Shapeless. У библиотеки имеется документация, правда, не очень обширная. Автор библиотеки — Сиддхартха Гаджил из Indian Institute of Science. Библиотека экспериментальная. Сам Сиддхартха говорит, что это пока не библиотека, а «work in progress». Глобальная цель библиотеки — брать статью живого математика, парсить текст, переводить естественный язык с формулами в формальные доказательства, которые мог бы чекать компилятор. Понятно, что до этого еще очень далеко. Пока что в библиотеке можно работать с зависимыми типами и основами гомотопической теории типов (HoTT), (полу-) автоматически доказывать теоремы.

Началось все с того, что мне захотелось записать вводный курс по зависимым типам на Скале для конкурса Степика. Не хотелось повторяться, на Идрисе недавно появился хороший курс. Скала была выбрана как один из самых популярных функциональных языков. Погуглил по гитхабу по словам «Скала», «зависимые типы», «HoTT» и наиболее многообещающе выглядела ProvingGround. Сразу дисклеймер — я не утверждаю, что те или иные языки или библиотеки наиболее подходят для программирования с зависимыми типами, автоматического доказательства теорем, работы с HoTT. Можно было взять другие языки или библиотеки — был бы другой курс.

Как известно, Скала — язык с ограниченной поддержкой зависимых типов. Зависимые типы имплементируются в ней (другая точка зрения — эмулируются) с помощью path-dependent типов, type-level значений и имплицитов. Объяснять зависимые типы на голой Скале или Скале плюс Shapeless и погрязнуть в технических деталях типа отличия type members от type parameters (дженериков), имплицитов, path-dependent типов, «Aux» паттерна, type-level вычислений и т.д. не очень хотелось. Поэтому часть курса была на голой Скале, но бОльшая часть практики — на ProvingGround.

Термы и типы

Для задания переменных, термов, типов, функций и т.д. ProvingGround предоставляет свой DSL.
Так можно объявить тип A и переменную a этого типа:

val A = "A" :: Type
val a = "a" :: A

т.е. типичное объявление выглядит как

val идентификатор_переменной = "как печатать переменную" :: Тип_переменной

Напечатать терм «красиво» можно с помощью метода .fansi, вывести его тип — с помощью .typ:

println(a)
> a : (A : U_0)
println(a.fansi)
> a
println(a.typ)
> A : U_0
println(a.typ.fansi)
> A

Можно задать переменную детальнее:

val a : Term = "a" :: A

Здесь A — это тип в библиотеке ProvingGround, т.е. HoTT-тип, а Term — это тип в Скале.

Итак, если мы задаем переменную, то пишем тип после ::, а если у нас уже есть терм, то проверить его тип можно с помощью !:

a !: A

То, что эта строчка компилируется, означает, что тип указан правильно.

Зависимые типы

Небольшое напоминание о типах. Есть значения и есть типы. У каждого значения есть его тип. Зависимый тип — это тип, зависящий от значения (другого типа). Например, список двух строк и список трех строк — это значения одного и того же типа — список строк. Но если вынести информацию о числе элементов на уровень типа, то получим зависимый тип — вектор (он зависит от значения — натурального числа). И вектор двух строк и вектор трех строк — разные типы. Еще примеры зависимых типов — ненулевое число, непустой список, пара чисел, где второе число меньше первого, тип-равенство 1 =:= 2 (у которого нет значений), типы 1 =:= 1, 2 =:= 2 (у которых по одному значению) и т.д.

Так можно задать зависимый тип Ba, который зависит от значений типа A, и переменную этого типа:

val Ba = "B(_ : A)" :: A ->: Type
val b = "b" :: Ba(a)

Функции

Теперь про стрелочки. Есть 4 основных типа стрелок для функций: :->, :~>, ->:, ~>: . С двоеточиями слева — для лямбд (т.е. самих функций), с двоеточиями справа — для типов функций. С дефисами — для обычных функций, с тильдами — для зависимых функций (т.е. у которых не только значение, но и тип значения зависит от аргумента). В качестве примера — тождественная функция

val id = A :~> (a :-> a) !: A ~>: (A ->: A)

Часть проверки типов осуществляется в рантайме, но часть информации о типах видит и компилятор Скалы:

val f : FuncLike[Term, Term] = a :~> b !: a ~>: Ba(a)
val f : Term => Term = a :~> b !: a ~>: Ba(a)

Здесь зависимый функциональный тип из ProvingGround/HoTT компилятор Скалы видит как обычную функцию в Скале.

Индуктивные типы

Можно задавать индуктивные типы. Например, булев тип с конструкторами «истина» и «ложь»:

val Bool = "Boolean" :: Type
val BoolInd = ("true" ::: Bool) |: ("false" ::: Bool) =: Bool
val tru :: fls :: HNil = BoolInd.intros

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

val идентификатор_объявления = (...) |: (...) |: (...) =: Имя_типа

где конструкторы значений этого типа отделены |: .

Еще пример — тип натуральных чисел с конструкторами «ноль» и «следующее число за натуральным n»:

val Nat = "Nat" :: Type
val NatInd = ("0" ::: Nat) |: ("succ" ::: Nat -->>: Nat) =: Nat
val zero :: succ :: HNil = NatInd.intros
val one = succ(zero) !: Nat
val two = succ(one) !: Nat
// ...

Тип целых чисел с конструкторами «плюс натуральное n» и «минус натуральное n минус 1» использует уже определенный тип натуральных чисел:

val Int = "Integer" :: Type
val IntInd = ("pos" ::: Nat ->>: Int) |: ("neg" ::: Nat ->>: Int) =: Int
val pos :: neg :: HNil = IntInd.intros

Тип списка значений типа A имеет конструкторы «пустой список» и «список с головой типа A и хвостом типа ListA»:

val ListA = "List(A)" :: Type
val ListAInd = ("nil" ::: ListA) |: ("cons" ::: A ->>: ListA -->>: ListA) =: ListA
val nil :: cons :: HNil = ListAInd.intros

У типа бинарного дерева (для простоты без значений некоторого типа в узлах) есть конструкторы «лист» и «вилка» (второй принимает пару поддеревьев):

val BTree = "BTree" :: Type
val BTreeInd = ("leaf" ::: BTree) |: ("fork" ::: BTree -->>: BTree -->>: BTree) =: BTree
val leaf :: fork :: HNil = BTreeInd.intros

Альтернативно конструктор «вилка» могла бы принимать функцию, которая переводит ложь в одно поддерево, истину в другое:

val BTree = "BTree" :: Type
val BTreeInd = ("leaf" ::: BTree) |: ("fork" ::: (Bool -|>: BTree) -->>: BTree) =: BTree
val leaf :: fork :: HNil = BTreeInd.intros

Зависимые индуктивные типы

Если тип зависимый (indexed inductive type), например вектор Vec или тип-равенство Id, то надо использовать =:: вместо =:, стрелку с тильдой и ссылаться на тип внутри конструкторов (Имя_типа -> Имя_типа(n)) в возвращаемом типе, (Имя_типа :> Имя_типа(n)) в принимаемом типе, а не просто Имя_типа(n). Например, тип вектора длины n:

val VecA = "Vec(A)" :: Nat ->: Type
val n = "n" :: Nat
val VecAInd = ("nil" ::: (VecA -> VecA(zero) )) |: 
    {"cons" ::: n ~>>: (A ->>: (VecA :> VecA(n) ) -->>: (VecA -> VecA(succ(n)) ))} =:: VecA
val vnil :: vcons :: HNil = VecAInd.intros

Еще один полезный зависимый тип позволяет формализовать понятие натурального числа, не превышающего другое натуральное число:

val Fin = "Fin" :: Nat ->: Type
val FinInd = {"FZ" ::: n ~>>: (Fin -> Fin(succ(n)) )} |: 
    {"FS" ::: n ~>>: ((Fin :> Fin(n) ) -->>: (Fin -> Fin(succ(n)) ))} =:: Fin
val fz :: fs :: HNil = FinInd.intros

Действительно, нет способа сконструировать значение типа Fin(zero). Есть ровно одно значение типа Fin(one):

val fz0 = fz(zero) !: Fin(one)

Есть ровно два значения типа Fin(two):

val fz1 = fz(one) !: Fin(two)
val fs1 = fs(one)(fz0) !: Fin(two)

Есть ровно три значения типа Fin(three):

fz(two) !: Fin(three)
fs(two)(fz1) !: Fin(three)
fs(two)(fs1) !: Fin(three)

и т.д.

Семейства индуктивных типов

Несколько слов об отличии семейства индуктивных типов (family of inductive types) от индексированного индуктивного типа (indexed inductive type). Например, List(A) — это семейство, а Vec(A)(n) — это семейство относительно типа A, но индексированный тип относительно натурального индекса n. Индуктивный тип — это тип, конструкторы которого для «следующих» значений могут использовать «предыдущие» значения (как у типов Nat, List и т.д.). Vec(A)(n) при фиксированном A является индуктивным типом, но не является при фиксированном n. В ProvingGround в настоящее время нет семейств индуктивных типов, т.е. нельзя, имея индуктивное определение, например, типа List(A), легко получить индуктивное определение типов List(B), List(Nat), List(Bool), List(List(A)) и т.д. Но можно эмулировать семейства с помощью индексированных типов:

val List = "List" :: Type ->: Type
val ListInd = {"nil" ::: A ~>>: (List -> List(A) )} |: 
    {"cons" ::: A ~>>: (A ->>: (List :> List(A) ) -->>: (List -> List(A) ))} =:: List
val nil :: cons :: HNil = ListInd.intros
cons(Nat)(zero)(cons(Nat)(one)(cons(Nat)(two)(nil(Nat)))) !: List(Nat)  // список 0, 1, 2

и

val Vec = "Vec" :: Type ->: Nat ->: Type
val VecInd = {"nil" ::: A ~>>: (Vec -> Vec(A)(zero) )} |: 
    {"cons" ::: A ~>>: n ~>>: (A ->>: (Vec :> Vec(A)(n) ) -->>: (Vec -> Vec(A)(succ(n)) ))} =:: Vec
val vnil :: vcons :: HNil = VecInd.intros
vcons(Bool)(two)(tru)(vcons(Bool)(one)(fls)(vcons(Bool)(zero)(tru)(vnil(Bool)))) !: Vec(Bool)(succ(two))  
// 3-элементный вектор tru, fls, tru

Можно также определить гетерогенный список (HList):

val HLst = "HList" :: Type ->: Type
val HLstInd = {"nil" ::: A ~>>: (HLst -> HLst(A) )} |: 
    {"cons" ::: A ~>>: (A ->>: (B ~>>: ((HLst :> HLst(B) ) -->>: (HLst -> HLst(A) ))))} =:: HLst
val hnil :: hcons :: HNil = HLstInd.intros

Мы сейчас реализовали собственный HList в библиотеке ProvingGround, которая написана поверх Shapeless, в которой основным строительным элементом является HList.

Алгебраические типы данных

В библиотеке можно эмулировать обобщенные алгебраические типы данных (GADT). Код, который выглядит на Хаскеле

{-# Language GADTs #-}
data Expr a where
    ELit     :: a         -> Expr a
    ESucc    :: Expr Int  -> Expr Int
    EIsZero  :: Expr Int  -> Expr Bool
    EIf      :: Expr Bool -> Expr a    -> Expr a    -> Expr a

и на чистой Скале

sealed trait Expr[A]
case class ELit[A](lit: A) extends Expr[A]
case class ESucc(num: Expr[Int]) extends Expr[Int]
case class EIsZero(num: Expr[Int]) extends Expr[Boolean]
case class EIf[A](cond: Expr[Boolean], thenExpr: Expr[A], elseExpr: Expr[A]) extends Expr[A]

запишется в ProvingGround как

val Expr = "Expr" :: Type ->: Type
val ExprInd = {"ELit" ::: A ~>>: (A ->>: (Expr -> Expr(A) ))} |:
  {"ESucc" ::: Expr(Nat) ->>: (Expr -> Expr(Nat) )} |:
  {"EIsZero" ::: Expr(Nat) ->>: (Expr -> Expr(Bool) )} |:
  {"EIf" ::: A ~>>: (Expr(Bool) ->>: Expr(A) ->>: Expr(A) ->>: (Expr -> Expr(A) ))} =:: Expr
val eLit :: eSucc :: eIsZero :: eIf :: HNil = ExprInd.intros

Классы типов

Также можно в библиотеке эмулировать классы типов. Например, функтор:

val A = "A" :: Type
val B = "B" :: Type
val C = "C" :: Type
val Functor = "Functor" :: (Type ->: Type) ->: Type
val F = "F(_ : U_0)" :: Type ->: Type
val Fmap = A ~>: (B ~>: ((A ->: B) ->: (F(A) ->: F(B) )))
val FunctorInd = {"functor" ::: F ~>>: (Fmap ->>: (Functor -> Functor(F) ))} =:: Functor
val functor :: HNil = FunctorInd.intros

Можно, например, список объявить экземпляром (instance) функтора:

val as = "as" :: List(A)
val indList_map = ListInd.induc(A :~> (as :-> (B ~>: ((A ->: B) ->: List(B) )))) // это индукция, о рекурсии и индукции идет речь ниже
val mapas = "map(as)" :: B ~>: ((A ->: B) ->: List(B))
val f = "f" :: A ->: B
val map = indList_map(A :~> (B :~> (f :->
       nil(B)
   )))(A :~> (a :-> (as :-> (mapas :-> (B :~> (f :->
       cons(B)(f(a))(mapas(B)(f))
   ))))))  !: A ~>: (List(A) ->: (B ~>: ((A ->: B) ->: List(B) )))
val listFunctor = functor(List)(A :~> (B :~> (f :-> (as :-> map(A)(as)(B)(f) )))) !: Functor(List)

Можно в класс типов добавить законы:

val fmap = "fmap" :: A ~>: (B ~>: ((A ->: B) ->: (F(A) ->: F(B) )))
val Fmap_id = A ~>: ( fmap(A)(A)(id(A)) =:= id(F(A)) )
val f = "f" :: A ->: B
val g = "g" :: B ->: C
val compose = A :~> (B :~> (C :~> (f :-> (g :-> (a :-> g(f(a)) 
    ))))) !: A ~>: (B ~>: (C ~>: ((A ->: B) ->: ((B ->: C) ->: (A ->: C)))))
val Fmap_compose = A ~>: (B ~>: (C ~>: (f ~>: (g ~>: ( 
    fmap(A)(C)(compose(A)(B)(C)(f)(g)) =:= compose(F(A))(F(B))(F(C))(fmap(A)(B)(f))(fmap(B)(C)(g)) )))))
val FunctorInd = {"functor" ::: F ~>>: (fmap ~>>: (Fmap_id ->>: (Fmap_compose ->>: (Functor -> Functor(F) ))))} =:: Functor
val functor :: HNil = FunctorInd.intros

Типы-равенства

В библиотеке уже есть встроенные сигма-тип (тип зависимой пары), пи-тип (тип зависимой функции, мы его уже видели выше), тип-равенство (identity type):

mkPair(a, b) !: Sgma(a !: A, Ba(a))
one.refl !: (one =:= one)
one.refl !: IdentityTyp(Nat, one, one)
two.refl !: (two =:= two)
(one =:= two) !: Type

но можно определить и свой, например, тип-равенство:

val Id = "Id" :: A ~>: (A ->: A ->: Type)
val IdInd = ("refl" ::: A ~>>: a ~>>: (Id -> Id(A)(a)(a) )) =:: Id
val refl :: HNil = IdInd.intros
refl(Nat)(two) !: Id(Nat)(two)(two)

Типы-равенства естественно возникают, когда начинается разговор о соответствии Карри-Ховарда. С одной стороны A ->: B — это функции из A в B, с другой — это логическая формула «из утверждения A следует B». И, с одной стороны, (A ->: B) ->: A ->: B — это тип функции высшего порядка, которая принимает на вход функцию A ->: B и значение типа A и возвращает эту функцию, примененную к этому значению, т.е. значение типа B. С другой стороны, это правило вывода в логике modus ponens — «если верно, что из A следует B, и верно A, то верно B». С такой точки зрения типы — это утверждения, а значения типов — это доказательства этих утверждений. И утверждение верно, если соответствующий тип населен, т.е. существует значение этого типа. Логическое «и» соответствует произведению типов, логическое «или» — сумме типов, логическое «не» — типу A ->: Zero, т.е. функциям в пустой тип. Так в теории типов возникает логика. Правда, не любая логика, а так называемая интуиционистская или конструктивная, т.е. логика без закона исключения третьего. Действительно, вообще говоря, нельзя сконструировать значение типа PlusTyp(A, A ->: Zero) (если не удалось доказать A, то это еще не значит, что удалось доказать не-A). Интересно, что справедливо отрицание к отрицанию закона исключения третьего:

val g = "g" :: PlusTyp(A, A ->: Zero) ->: Zero
val g1 = a :-> g(PlusTyp(A, A ->: Zero).incl1(a)) !: A ->: Zero
g :-> g(PlusTyp(A, A ->: Zero).incl2(g1)) !: (PlusTyp(A, A ->: Zero) ->: Zero) ->: Zero

Ну так вот, если типы — утверждения, а значения типов — доказательства, то раз равенство двух термов a1 =:= a2 — это утверждение, значит и тип. Тип зависимый, т.к. зависит от значений a1, a2 некоторого типа A. Если a1, a2 разные, то не должно быть способа сконструировать значение этого типа, т.к. утверждение ложно. Если одинаковые, то наоборот должен быть способ сконструировать значение, раз утверждение верно, так что у нашего индуктивного типа единственный конструктор refl(A)(a) !: Id(A)(a)(a) (или a.refl !: (a =:= a) для встроенного типа-равенства).

Еще один полезный тип при доказательстве теорем с неравенствами:

val LTE = "?" :: Nat ->: Nat ->: Type
val LTEInd = {"0 ? _" ::: m ~>>: (LTE -> LTE(zero)(m) )} |: 
    {"S _ ? S _" ::: n ~>>: m ~>>: ((LTE :> LTE(n)(m) ) -->>: (LTE -> LTE(succ(n))(succ(m)) ))} =:: LTE
val lteZero :: lteSucc :: HNil = LTEInd.intros

Высшие индуктивные типы

Еще в библиотеке можно работать с высшими индуктивными типами. Например, окружностью

val Circle = "S^1" :: Type
val base = "base" :: Circle // конструктор
val loop = "loop" :: (base =:= base) // еще один конструктор

и сферой

val Sphere = "S^2" :: Type
val base = "base" :: Sphere // конструктор
val surf = "surf" :: (base.refl =:= base.refl) // еще один конструктор
//  val surf = "surf" :: IdentityTyp(base =:= base, base.refl, base.refl)
//  val surf = "surf" :: IdentityTyp(IdentityTyp(Sphere, base, base), base.refl, base.refl)

Рекурсия и индукция

Теперь о том, как определять (рекурсивные) функции. Библиотека для каждого индуктивного типа генерирует методы .rec, .induc, т.е. рекурсию (aka рекурсор) и индукцию — элиминаторы в постоянный и зависимый тип соответственно, с помощью которых можно осуществлять сопоставление с образцом (pattern matching), если надо — рекурсивное. Например, можно определить логическое «не»:

val b = "b" :: Bool
val recBB = BoolInd.rec(Bool)
val not = recBB(fls)(tru)

Здесь можно считать, что мы сделали сопоставление с образцом:

match {
  case true => false
  case false => true
}

Проверяем, что всё работает:

not(tru) == fls
not(fls) == tru

Также можно определить логическое «и»:

val recBBB = BoolInd.rec(Bool ->: Bool)
val and = recBBB(b :-> b)(b :-> fls)

Здесь можно считать, что мы сделали сопоставление с образцом по первому аргументу:

// псевдокод
match {
  case true => (b => b)
  case false => (b => false)
}

Проверяем:

and(fls)(tru) == fls
and(tru)(tru) == tru

Можно определить удваивание натурального числа:

val n = "n" :: Nat
val m = "m" :: Nat
val recNN = NatInd.rec(Nat)
val double = recNN(zero)(n :-> (m :-> succ(succ(m)) ))

Здесь опять можно считать, что мы сделали сопоставление с образцом:

// псевдокод
match {
  case Zero => Zero
  case Succ(n) =>
    val m = double(n)
    m + 2
}

Проверяем:

println(double(two).fansi)
> succ(succ(succ(succ(0))))

Определим сложение натуральных чисел:

val recNNN = NatInd.rec(Nat ->: Nat)
val addn = "add(n)" :: Nat ->: Nat
val add = recNNN(m :-> m)(n :-> (addn :-> (m :-> succ(addn(m)) )))

Здесь аналогично можно считать, что мы сделали сопоставление с образцом по первому аргументу:

// псевдокод
match {
  case Zero => (m => m)
  case Succ(n) =>
    val addn = add(n)
    m => addn(m) + 1
}

Проверка:

println(add(two)(three).fansi)
> succ(succ(succ(succ(succ(0)))))

Определим также конкатенацию векторов:

val vn = "v_n" :: VecA(n)
val vm = "v_m" :: VecA(m)
val indVVV = VecAInd.induc(n :~> (vn :-> (m ~>: (VecA(m) ->: VecA(add(n)(m)) ))))
val concatVn = "concat(v_n)" :: (m ~>: (VecA(m) ->: VecA(add(n)(m)) ))
val vconcat = indVVV(m :~> (vm :-> vm))(n :~> (a :-> (vn :-> (concatVn :-> (m :~> (vm :-> 
    vcons(add(n)(m))(a)(concatVn(m)(vm)) ))))))

Здесь мы используем не рекурсию, а индукцию, т.к. нам нужен элиминатор в зависимый тип
m ~>: (VecA(m) ->: VecA(add(n)(m))) — действительно, этот тип зависит от n из вектора (первый аргумент конкатенации), который мы деконструируем при сопоставлении с образцом:

// псевдокод
match {
  case (Zero, Nil) => (vm => vm)
  case (Succ(n), Cons(a)(vn)) =>
    val concatVn = concat(vn)
    vm => Cons(a)(concatVn(vm))
}

Тестируем:

val a = "a" :: A
val a1 = "a1" :: A
val a2 = "a2" :: A
val a3 = "a3" :: A
val a4 = "a4" :: A
val vect = vcons(one)(a)(vcons(zero)(a1)(vnil))
val vect1 = vcons(two)(a2)(vcons(one)(a3)(vcons(zero)(a4)(vnil)))
println(vconcat(two)(vect)(three)(vect1).fansi)
> cons(succ(succ(succ(succ(0)))))(a)(cons(succ(succ(succ(0))))(a1)(cons(succ(succ(0)))(a2)(cons(succ(0))(a3)(cons(0)(a4)(nil)))))

Покажу еще пример, как теоремы доказываются в ProvingGround. Докажем, что add(n)(n) =:= double(n).

val indN_naddSm_eq_S_naddm = NatInd.induc(n :-> (m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) )))
val hyp1 = "n+Sm=S(n+m)" :: (m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) ))
val lemma = indN_naddSm_eq_S_naddm(m :~> succ(m).refl)(n :~> (hyp1 :-> (m :~>
    IdentityTyp.extnslty(succ)( add(n)(succ(m)) )( succ(add(n)(m)) )( hyp1(m) )
  )))  !: n ~>: m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) )
val lemma1 = IdentityTyp.extnslty(succ)( add(n)(succ(n)) )( succ(add(n)(n)) )( lemma(n)(n) )
val indN_naddn_eq_2n = NatInd.induc(n :-> ( add(n)(n) =:= double(n) ))
val hyp = "n+n=2*n" :: ( add(n)(n) =:= double(n) )
val lemma2 = IdentityTyp.extnslty( m :-> succ(succ(m)) )( add(n)(n) )( double(n) )(hyp)
indN_naddn_eq_2n(zero.refl)(n :~> (hyp :->
    IdentityTyp.trans(Nat)( add(succ(n))(succ(n)) )( succ(succ(add(n)(n))) )( double(succ(n)) )(lemma1)(lemma2)
  ))  !: n ~>: ( add(n)(n) =:= double(n) )

Окружность не получается определить как обычный индуктивный тип через (...) |: (...) =:: ... (действительно, конструктор loop возвращает не значение типа Circle, как было бы для обычного индуктивного типа). Поэтому и рекурсию с индукцией приходится определять вручную:

val recCirc = "rec_{S^1}" :: A ~>: a ~>: (a =:= a) ->: Circle ->: A
val B = "B(_ : S^1)" :: Circle ->: Type
val b = "b" :: B(base)
val c = "c" :: Circle
val indCirc = "ind_{S^1}" :: B ~>: b ~>: (( IdentityTyp.transport(B)(base)(base)(loop)(b) =:= b ) ->: c ~>: B(c) )

с двумя аксиомами comp_base и comp_loop:

val l = "l" :: ( IdentityTyp.transport(B)(base)(base)(loop)(b) =:= b )
val comp_base = "comp_base" :: B ~>: b ~>: l ~>: ( indCirc(B)(b)(l)(base) =:= b )
val P = "P(_ : A)" :: A ->: Type
val f = "f" :: a ~>: P(a)
val dep_map = "dep_map" :: A ~>: (P ~>: (f ~>: (a ~>: (a1 ~>: (( a =:= a1 ) ->: ( f(a) =:= f(a1) )))))) // dep_map аналогично IdentityTyp.extnslty(f), но для зависимой f
val comp_loop = "comp_loop" :: B ~>: b ~>: l ~>: ( dep_map(Circle)(B)(indCirc(B)(b)(l))(base)(base)(loop) =:= l )

Несколько слов о том, как запускать код на ProvingGround. Есть 3 способа.

1. Первый и рекомендуемый — из консоли (загружается Ammonite REPL) с помощью команды
   sbt mantle/test:run (из корня проекта ProvingGround после клонирования репозитория github.com/siddhartha-gadgil/ProvingGround.git, в случае ошибки запуска Ammonite REPL создать пустую директорию ProvingGround/mantle/target/web/classes/test).
   
   
2. Второй — с помощью команды sbt server/run и затем открыть в браузере http://localhost:8080.
   
   
3. Третий — из IDE. В IntelliJ Idea 2017.1.3 проект может импортироваться после модификации build.sbt, но код может не запускаться. Решение — импортировать в Идею не весь проект, а только подпроект ProvingGround/core. Для этого нужно положить новый build.sbt сюда: ProvingGround/core/build.sbt .
   
   Список импортов:
   
   

   import provingground._
   import HoTT._
   import TLImplicits._
   import shapeless._
   //import ammonite.ops._
   import FansiShow._

Если кому интересна эта тема (теория типов, гомотопическая теория типов, зависимые типы, вычисления на уровне типов, автоматическое доказательство теорем), добро пожаловать на мой курс. Он вводный. По HoTT скорее даже не введение, а введение во введение, но по остальным направлениям, думаю, дотягивает до уровня просто введения. Спасибо за внимание.