Scala + Shapeless + ProvingGroundの依存型からホモトピー型理論まで

みなさんこんにちは。 Shapelessを使用してRockで記述されたProvingGroundライブラリを使用した私の経験を共有したいと思います。 ライブラリにはドキュメントがありますが 、それほど広範囲ではありません。 図書館の著者は、インド科学研究所のシッダールタガジルです。 ライブラリは実験的です。 シッダールタ自身は、これはまだ図書館ではなく、「進行中の作業」だと言っています。 ライブラリのグローバルな目標は、生きている数学者から記事を取り出し、テキストを解析し、自然言語を式で変換して、コンパイラがチェックできる形式的な証明にすることです。 これはまだ非常に遠いことは明らかです。 これまでのところ、ライブラリでは、依存型およびホモトピー型理論（ HoTT ）の基本を使用して、（半）定理を自動的に証明できます。

それはすべて、StepikaコンテストのRockで依存型に関する入門コースを記録したかったという事実から始まりました。 繰り返したくありませんでしたが、最近、イドリスに良いコースが登場しました。 Scalaは、最も一般的な関数型言語の1つとして選ばれました。 「Scala」、「dependent types」、「HoTT」および最も有望な外観のProvingGroundに従ってgithubでGoogleを検索しました。 すぐに免責事項-特定の言語やライブラリが、依存型を使用したプログラミング、自動定理の証明、HoTTの操作に最も適しているとは主張しません。 他の言語やライブラリを使用することもできます-別のコースがあります。

ご存じのように、Scalaは依存型のサポートが制限されている言語です。 依存型は、 パス依存型 、 型レベル値、および含意を使用して実装されます（ 別の観点がエミュレートされます）。 ベアロックまたはロックプラスシェイプレスの依存型を説明し、型パラメーター（ジェネリック）からの型メンバーの違い 、含意、パス依存型、 「補助」パターン 、型レベルの計算などの技術的詳細に行き詰まります。 私は本当にしたくありませんでした。 したがって、コースの一部はむき出しのロックで行われましたが、練習のほとんどはProvingGroundで行われました。

用語と種類

変数、用語、タイプ、関数などを設定するには ProvingGroundはDSLを提供します。
したがって、タイプAとこのタイプの変数を宣言できます。

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

つまり 典型的な広告は次のようになります

 val _ = "  " :: _ 

.fansiメソッドを使用して「美しく」という用語を.fansiし、 .fansiを使用してそのタイプを印刷でき.fansi 。

 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はScalaのタイプです。

そのため、変数を設定した場合、 ::後に型を記述し、すでに用語がある場合は、その型を!:確認でき!:

 a !: A 

この行がコンパイルされているという事実は、タイプが正しく指定されていることを意味します。

依存型

タイプを少し思い出してください。 値があり、タイプがあります。 各値にはタイプがあります。 依存型は、値依存型 （別の型の）です。 たとえば、2行のリストと3行のリストは、同じタイプの値（行のリスト）です。 しかし、要素の数に関する情報を型レベルに渡すと、従属型-ベクトル（値に依存-自然数）が得られます。 また、2行のベクトルと3行のベクトルは異なるタイプです。 依存型の他の例としては、ゼロ以外の数値、空でないリスト、2番目の数値が最初の数値より小さい数値のペア、等値タイプ1 =:= 2 （値なし）、タイプ1 =:= 1 2 =:= 2 （これ1つの値）など

したがって、タイプAの値とこのタイプの変数に依存する依存タイプBa設定できます。

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

機能

次に矢印について。 機能の矢印には、主に4つのタイプがあり~>: ->: ~>: 、 ->: ~>: 左側にコロンを-ラムダ（つまり関数自体）に、右側にコロンを-関数のタイプに。 ハイフンを使用-通常の関数の場合、チルダを使用-依存関数の場合（つまり、値だけでなく値のタイプも引数に依存します）。 例として、同一の機能

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

型チェックの一部は実行時に行われますが、Scalaコンパイラーは型情報の一部も確認します。

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

ここでは、RockのProvingGround / HoTTコンパイラの従属関数タイプは、Rockの通常の関数と見なしています。

誘導型

誘導タイプを指定できます。 たとえば、コンストラクターが「true」および「false」であるブール型：

 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 // ... 

コンストラクター「plus integer n 」および「minus integer n minus 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 

バイナリツリータイプ（簡単にするため、ノードに特定のタイプの値を持たない）には、コンストラクター「リーフ」と「フォーク」があります（2番目はサブツリーのペアを取ります）。

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

あるいは、プラグコンストラクターは、嘘を1つのサブツリーに変換し、真実を別のサブツリーに変換する関数を取ることができます。

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

依存する誘導型

型がインデックス付き誘導型 、たとえば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)型の値は1つだけですFin(one) 。

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

タイプFin(two)値は正確に2つあります。

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

タイプFin(three)値は正確に3つあります。

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

など

誘導型ファミリー

帰納的タイプのファミリーとインデックス付きの帰納的タイプの違いについてのいくつかの言葉。 たとえば、 List(A)はファミリであり、 Vec(A)(n)はタイプAに関連するファミリですが、インデックス付きタイプは自然インデックスnます。 帰納的型は、コンストラクタが「次の」値に「前の」値を使用できる型です（ Nat 、 Listなどの型と同様）。 固定A Vec(A)(n)は誘導型ですが、固定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ライブラリに独自のHListを実装しました。これはShapelessの上に記述されており、メインの構築要素はHListです。

代数データ型

ライブラリは、一般化された代数データ型（ GADT ）をエミュレートできます。 Haskellコード

 {-# 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 

たとえば、リストをファンクターのインスタンスとして宣言できます。

 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 

平等タイプ

ライブラリには、組み込みのシグマ型（依存ペアの型）、pi型（依存関数の型、上で既に見た）、ID型が既にあります。

 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への関数であり、他方では、「fromステートメントAはB続く」という論理式です。 そして、一方で、 (A ->: B) ->: A ->: Bは、入力関数A ->: BおよびタイプA値を受け取り、それに適用されるこの関数を返す高階関数のタイプです。値、つまり タイプB値B 一方、これは、法則ポネンスロジックの推論規則です。「 AがAから続き、 Aが真である場合、 Bは真です。」 この観点から、タイプはステートメントであり、タイプ値はこれらのステートメントの証拠です。 そして、対応するタイプが入力されている場合、つまり このタイプの値があります。 論理「and」は型の積に、論理「or」は型の合計に、論理「not」は型A ->: Zeroに対応します。 空の型に機能します。 したがって、型理論には論理があります。 真実ではなく、論理ではなく、いわゆる直観主義的または建設的、すなわち 第三の排除の法則のない論理。 実際、一般的に言えば、 PlusTyp(A, A ->: Zero)型の値を構築することはできませんPlusTyp(A, A ->: Zero) （ Aを証明できなかった場合、これはPlusTyp(A, A ->: Zero)を証明できたという意味ではありません）。 興味深いことに、3番目の排除法の否定は真実です。

 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 

タイプがステートメントであり、タイプの値が証明である場合、2つの用語a1 =:= a2の等価性はステートメントであるため、タイプを意味します。 タイプが依存しているのは、 タイプA値a1, a2依存しますA a1, a2異なる場合、このタイプの値を構築する方法はないはずです。 ステートメントは偽です。 それらが同じ場合、反対に、ステートメントがtrueであるため、値を構築する方法があるはずです。そのため、誘導型にはコンストラクター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) 

再帰と帰納

（再帰）関数を定義する方法について説明します。 各帰納的タイプのライブラリは、 .induc 、 .induc 、つまり 再帰（別名再帰）および誘導-定数および依存型へのエリミネーター。それぞれ、必要に応じて再帰的にパターンマッチングを実行できます。 たとえば、論理的な「not」を定義できます。

 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 

論理的な「and」も定義できます。

 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 

自然数の2倍を決定できます。

 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) ) 

2つの公理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：実行します （ github.com/siddhartha-gadgil/ProvingGround.gitリポジトリを複製した後、ProvingGroundプロジェクトのルートから、Ammonite REPLの起動に失敗した場合、空のディレクトリProvingGround/mantle/target/web/classes/test ）。
   
   
2. 2番目は、 sbt server/runコマンドを使用してから、ブラウザーでhttp：// localhost：8080を開きます 。
   
   
3. 3番目はIDEからのものです。 IntelliJ Idea 2017.1.3では、build.sbtの変更後にプロジェクトがインポートされる場合がありますが、コードが起動しない場合があります。 解決策は、プロジェクト全体ではなく、 ProvingGround/coreサブプロジェクトのみをIdeaにインポートすることです。 これを行うには、 新しいbuild.sbtを ProvingGround/core/build.sbtます。
   
   インポートのリスト：
   
   

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

このトピック（型理論、ホモトピー型理論、依存型、型レベル計算、定理の自動証明）に興味がある人は、私のコースへようこそ。 彼は入門です。 HoTTによれば、それはおそらく序論ではなく、序論への序論ですが、他の分野では、序論のレベルに達していると思います。 ご清聴ありがとうございました。