{"id":286672,"date":"2017-05-22T13:15:02","date_gmt":"2017-05-22T09:15:02","guid":{"rendered":"http:\/\/savepearlharbor.com\/?p=286672"},"modified":"-0001-11-30T00:00:00","modified_gmt":"2017-05-22T09:15:02","slug":"","status":"publish","type":"post","link":"https:\/\/savepearlharbor.com\/?p=286672","title":{"rendered":"\u041e\u0442 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432 \u043a \u0433\u043e\u043c\u043e\u0442\u043e\u043f\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0442\u0435\u043e\u0440\u0438\u0438 \u0442\u0438\u043f\u043e\u0432 \u043d\u0430 Scala + Shapeless + ProvingGround"},"content":{"rendered":"

\u0412\u0441\u0435\u043c \u043f\u0440\u0438\u0432\u0435\u0442. \u0425\u043e\u0447\u0443 \u043f\u043e\u0434\u0435\u043b\u0438\u0442\u044c\u0441\u044f \u0441\u0432\u043e\u0438\u043c \u043e\u043f\u044b\u0442\u043e\u043c \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u044f \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 ProvingGround<\/a>, \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043d\u043e\u0439 \u043d\u0430 \u0421\u043a\u0430\u043b\u0435 \u0441 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c Shapeless<\/a>. \u0423 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 \u0438\u043c\u0435\u0435\u0442\u0441\u044f \u0434\u043e\u043a\u0443\u043c\u0435\u043d\u0442\u0430\u0446\u0438\u044f<\/a>, \u043f\u0440\u0430\u0432\u0434\u0430, \u043d\u0435 \u043e\u0447\u0435\u043d\u044c \u043e\u0431\u0448\u0438\u0440\u043d\u0430\u044f. \u0410\u0432\u0442\u043e\u0440 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 \u2014 \u0421\u0438\u0434\u0434\u0445\u0430\u0440\u0442\u0445\u0430 \u0413\u0430\u0434\u0436\u0438\u043b<\/a> \u0438\u0437 Indian Institute of Science. \u0411\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 \u044d\u043a\u0441\u043f\u0435\u0440\u0438\u043c\u0435\u043d\u0442\u0430\u043b\u044c\u043d\u0430\u044f. \u0421\u0430\u043c \u0421\u0438\u0434\u0434\u0445\u0430\u0440\u0442\u0445\u0430 \u0433\u043e\u0432\u043e\u0440\u0438\u0442, \u0447\u0442\u043e \u044d\u0442\u043e \u043f\u043e\u043a\u0430 \u043d\u0435 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430, \u0430 \u00abwork in progress\u00bb. \u0413\u043b\u043e\u0431\u0430\u043b\u044c\u043d\u0430\u044f \u0446\u0435\u043b\u044c \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 \u2014 \u0431\u0440\u0430\u0442\u044c \u0441\u0442\u0430\u0442\u044c\u044e \u0436\u0438\u0432\u043e\u0433\u043e \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0430, \u043f\u0430\u0440\u0441\u0438\u0442\u044c \u0442\u0435\u043a\u0441\u0442, \u043f\u0435\u0440\u0435\u0432\u043e\u0434\u0438\u0442\u044c \u0435\u0441\u0442\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u044b\u0439 \u044f\u0437\u044b\u043a \u0441 \u0444\u043e\u0440\u043c\u0443\u043b\u0430\u043c\u0438 \u0432 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043c\u043e\u0433 \u0431\u044b \u0447\u0435\u043a\u0430\u0442\u044c \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0442\u043e\u0440. \u041f\u043e\u043d\u044f\u0442\u043d\u043e, \u0447\u0442\u043e \u0434\u043e \u044d\u0442\u043e\u0433\u043e \u0435\u0449\u0435 \u043e\u0447\u0435\u043d\u044c \u0434\u0430\u043b\u0435\u043a\u043e. \u041f\u043e\u043a\u0430 \u0447\u0442\u043e \u0432 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435 \u043c\u043e\u0436\u043d\u043e \u0440\u0430\u0431\u043e\u0442\u0430\u0442\u044c \u0441 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u043c\u0438 \u0442\u0438\u043f\u0430\u043c\u0438 \u0438 \u043e\u0441\u043d\u043e\u0432\u0430\u043c\u0438 \u0433\u043e\u043c\u043e\u0442\u043e\u043f\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0442\u0435\u043e\u0440\u0438\u0438 \u0442\u0438\u043f\u043e\u0432 (HoTT<\/a>), (\u043f\u043e\u043b\u0443-) \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u0442\u0435\u043e\u0440\u0435\u043c\u044b.
<\/a>
\u041d\u0430\u0447\u0430\u043b\u043e\u0441\u044c \u0432\u0441\u0435 \u0441 \u0442\u043e\u0433\u043e, \u0447\u0442\u043e \u043c\u043d\u0435 \u0437\u0430\u0445\u043e\u0442\u0435\u043b\u043e\u0441\u044c \u0437\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u0432\u0432\u043e\u0434\u043d\u044b\u0439 \u043a\u0443\u0440\u0441 \u043f\u043e \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u043c \u0442\u0438\u043f\u0430\u043c \u043d\u0430 \u0421\u043a\u0430\u043b\u0435 \u0434\u043b\u044f \u043a\u043e\u043d\u043a\u0443\u0440\u0441\u0430 \u0421\u0442\u0435\u043f\u0438\u043a\u0430. \u041d\u0435 \u0445\u043e\u0442\u0435\u043b\u043e\u0441\u044c \u043f\u043e\u0432\u0442\u043e\u0440\u044f\u0442\u044c\u0441\u044f, \u043d\u0430 \u0418\u0434\u0440\u0438\u0441\u0435 \u043d\u0435\u0434\u0430\u0432\u043d\u043e \u043f\u043e\u044f\u0432\u0438\u043b\u0441\u044f \u0445\u043e\u0440\u043e\u0448\u0438\u0439 \u043a\u0443\u0440\u0441<\/a>. \u0421\u043a\u0430\u043b\u0430 \u0431\u044b\u043b\u0430 \u0432\u044b\u0431\u0440\u0430\u043d\u0430 \u043a\u0430\u043a \u043e\u0434\u0438\u043d \u0438\u0437 \u0441\u0430\u043c\u044b\u0445 \u043f\u043e\u043f\u0443\u043b\u044f\u0440\u043d\u044b\u0445 \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u044b\u0445 \u044f\u0437\u044b\u043a\u043e\u0432. \u041f\u043e\u0433\u0443\u0433\u043b\u0438\u043b \u043f\u043e \u0433\u0438\u0442\u0445\u0430\u0431\u0443 \u043f\u043e \u0441\u043b\u043e\u0432\u0430\u043c \u00ab\u0421\u043a\u0430\u043b\u0430\u00bb, \u00ab\u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0435 \u0442\u0438\u043f\u044b\u00bb, \u00abHoTT\u00bb \u0438 \u043d\u0430\u0438\u0431\u043e\u043b\u0435\u0435 \u043c\u043d\u043e\u0433\u043e\u043e\u0431\u0435\u0449\u0430\u044e\u0449\u0435 \u0432\u044b\u0433\u043b\u044f\u0434\u0435\u043b\u0430 ProvingGround. \u0421\u0440\u0430\u0437\u0443 \u0434\u0438\u0441\u043a\u043b\u0435\u0439\u043c\u0435\u0440 \u2014 \u044f \u043d\u0435 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0430\u044e, \u0447\u0442\u043e \u0442\u0435 \u0438\u043b\u0438 \u0438\u043d\u044b\u0435 \u044f\u0437\u044b\u043a\u0438 \u0438\u043b\u0438 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 \u043d\u0430\u0438\u0431\u043e\u043b\u0435\u0435 \u043f\u043e\u0434\u0445\u043e\u0434\u044f\u0442 \u0434\u043b\u044f \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u043c\u0438 \u0442\u0438\u043f\u0430\u043c\u0438, \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c, \u0440\u0430\u0431\u043e\u0442\u044b \u0441 HoTT. \u041c\u043e\u0436\u043d\u043e \u0431\u044b\u043b\u043e \u0432\u0437\u044f\u0442\u044c \u0434\u0440\u0443\u0433\u0438\u0435 \u044f\u0437\u044b\u043a\u0438 \u0438\u043b\u0438 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 \u2014 \u0431\u044b\u043b \u0431\u044b \u0434\u0440\u0443\u0433\u043e\u0439 \u043a\u0443\u0440\u0441. <\/p>\n

\u041a\u0430\u043a \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u043e, \u0421\u043a\u0430\u043b\u0430 \u2014 \u044f\u0437\u044b\u043a \u0441 \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u043e\u0439 \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u043a\u043e\u0439 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432. \u0417\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0435 \u0442\u0438\u043f\u044b \u0438\u043c\u043f\u043b\u0435\u043c\u0435\u043d\u0442\u0438\u0440\u0443\u044e\u0442\u0441\u044f \u0432 \u043d\u0435\u0439 (\u0434\u0440\u0443\u0433\u0430\u044f<\/a> \u0442\u043e\u0447\u043a\u0430 \u0437\u0440\u0435\u043d\u0438\u044f \u2014 \u044d\u043c\u0443\u043b\u0438\u0440\u0443\u044e\u0442\u0441\u044f) \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e path-dependent \u0442\u0438\u043f\u043e\u0432<\/a>, type-level<\/a> \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 \u0438 \u0438\u043c\u043f\u043b\u0438\u0446\u0438\u0442\u043e\u0432<\/a>. \u041e\u0431\u044a\u044f\u0441\u043d\u044f\u0442\u044c \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0435 \u0442\u0438\u043f\u044b \u043d\u0430 \u0433\u043e\u043b\u043e\u0439 \u0421\u043a\u0430\u043b\u0435 \u0438\u043b\u0438 \u0421\u043a\u0430\u043b\u0435 \u043f\u043b\u044e\u0441 Shapeless \u0438 \u043f\u043e\u0433\u0440\u044f\u0437\u043d\u0443\u0442\u044c \u0432 \u0442\u0435\u0445\u043d\u0438\u0447\u0435\u0441\u043a\u0438\u0445 \u0434\u0435\u0442\u0430\u043b\u044f\u0445 \u0442\u0438\u043f\u0430 \u043e\u0442\u043b\u0438\u0447\u0438\u044f<\/a> type members \u043e\u0442 type parameters (\u0434\u0436\u0435\u043d\u0435\u0440\u0438\u043a\u043e\u0432), \u0438\u043c\u043f\u043b\u0438\u0446\u0438\u0442\u043e\u0432, path-dependent \u0442\u0438\u043f\u043e\u0432, \u00abAux\u00bb \u043f\u0430\u0442\u0442\u0435\u0440\u043d\u0430<\/a>, type-level \u0432\u044b\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u0439 \u0438 \u0442.\u0434. \u043d\u0435 \u043e\u0447\u0435\u043d\u044c \u0445\u043e\u0442\u0435\u043b\u043e\u0441\u044c. \u041f\u043e\u044d\u0442\u043e\u043c\u0443 \u0447\u0430\u0441\u0442\u044c \u043a\u0443\u0440\u0441\u0430 \u0431\u044b\u043b\u0430 \u043d\u0430 \u0433\u043e\u043b\u043e\u0439 \u0421\u043a\u0430\u043b\u0435, \u043d\u043e \u0431\u041e\u043b\u044c\u0448\u0430\u044f \u0447\u0430\u0441\u0442\u044c \u043f\u0440\u0430\u043a\u0442\u0438\u043a\u0438 \u2014 \u043d\u0430 ProvingGround.<\/p>\n

\u0422\u0435\u0440\u043c\u044b \u0438 \u0442\u0438\u043f\u044b<\/h4>\n

\u0414\u043b\u044f \u0437\u0430\u0434\u0430\u043d\u0438\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445, \u0442\u0435\u0440\u043c\u043e\u0432, \u0442\u0438\u043f\u043e\u0432, \u0444\u0443\u043d\u043a\u0446\u0438\u0439 \u0438 \u0442.\u0434. ProvingGround \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u0432\u043e\u0439 DSL<\/acronym>.
\u0422\u0430\u043a \u043c\u043e\u0436\u043d\u043e \u043e\u0431\u044a\u044f\u0432\u0438\u0442\u044c \u0442\u0438\u043f A<\/code> \u0438 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u0443\u044e a<\/code> \u044d\u0442\u043e\u0433\u043e \u0442\u0438\u043f\u0430:<\/p>\n

val A = "A" :: Type val a = "a" :: A<\/code><\/pre>\n
  \u0442.\u0435. \u0442\u0438\u043f\u0438\u0447\u043d\u043e\u0435 \u043e\u0431\u044a\u044f\u0432\u043b\u0435\u043d\u0438\u0435 \u0432\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u043a\u0430\u043a<\/p>\n
val \u0438\u0434\u0435\u043d\u0442\u0438\u0444\u0438\u043a\u0430\u0442\u043e\u0440_\u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 = "\u043a\u0430\u043a \u043f\u0435\u0447\u0430\u0442\u0430\u0442\u044c \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u0443\u044e" :: \u0422\u0438\u043f_\u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439<\/code><\/pre>\n
  \u041d\u0430\u043f\u0435\u0447\u0430\u0442\u0430\u0442\u044c \u0442\u0435\u0440\u043c \u00ab\u043a\u0440\u0430\u0441\u0438\u0432\u043e\u00bb \u043c\u043e\u0436\u043d\u043e \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043c\u0435\u0442\u043e\u0434\u0430 .fansi<\/code>, \u0432\u044b\u0432\u0435\u0441\u0442\u0438 \u0435\u0433\u043e \u0442\u0438\u043f \u2014 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e .typ<\/code>:<\/p>\n
println(a) > a : (A : U_0) println(a.fansi) > a println(a.typ) > A : U_0 println(a.typ.fansi) > A<\/code><\/pre>\n
  \u041c\u043e\u0436\u043d\u043e \u0437\u0430\u0434\u0430\u0442\u044c \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u0443\u044e \u0434\u0435\u0442\u0430\u043b\u044c\u043d\u0435\u0435:<\/p>\n
val a : Term = "a" :: A<\/code><\/pre>\n
  \u0417\u0434\u0435\u0441\u044c A<\/code> \u2014 \u044d\u0442\u043e \u0442\u0438\u043f \u0432 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435 ProvingGround, \u0442.\u0435. HoTT<\/acronym>-\u0442\u0438\u043f, \u0430 Term<\/code> \u2014 \u044d\u0442\u043e \u0442\u0438\u043f \u0432 \u0421\u043a\u0430\u043b\u0435.<\/p>\n
  \u0418\u0442\u0430\u043a, \u0435\u0441\u043b\u0438 \u043c\u044b \u0437\u0430\u0434\u0430\u0435\u043c \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u0443\u044e, \u0442\u043e \u043f\u0438\u0448\u0435\u043c \u0442\u0438\u043f \u043f\u043e\u0441\u043b\u0435 ::<\/code>, \u0430 \u0435\u0441\u043b\u0438 \u0443 \u043d\u0430\u0441 \u0443\u0436\u0435 \u0435\u0441\u0442\u044c \u0442\u0435\u0440\u043c, \u0442\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c \u0435\u0433\u043e \u0442\u0438\u043f \u043c\u043e\u0436\u043d\u043e \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e !:<\/code><\/p>\n
a !: A<\/code><\/pre>\n
  \u0422\u043e, \u0447\u0442\u043e \u044d\u0442\u0430 \u0441\u0442\u0440\u043e\u0447\u043a\u0430 \u043a\u043e\u043c\u043f\u0438\u043b\u0438\u0440\u0443\u0435\u0442\u0441\u044f, \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e \u0442\u0438\u043f \u0443\u043a\u0430\u0437\u0430\u043d \u043f\u0440\u0430\u0432\u0438\u043b\u044c\u043d\u043e.<\/p>\n
\u0417\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0435 \u0442\u0438\u043f\u044b<\/h4>\n
  \u041d\u0435\u0431\u043e\u043b\u044c\u0448\u043e\u0435 \u043d\u0430\u043f\u043e\u043c\u0438\u043d\u0430\u043d\u0438\u0435 \u043e \u0442\u0438\u043f\u0430\u0445. \u0415\u0441\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0438 \u0435\u0441\u0442\u044c \u0442\u0438\u043f\u044b. \u0423 \u043a\u0430\u0436\u0434\u043e\u0433\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0435\u0441\u0442\u044c \u0435\u0433\u043e \u0442\u0438\u043f. \u0417\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0439 \u0442\u0438\u043f<\/a> \u2014 \u044d\u0442\u043e \u0442\u0438\u043f, \u0437\u0430\u0432\u0438\u0441\u044f\u0449\u0438\u0439 \u043e\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f (\u0434\u0440\u0443\u0433\u043e\u0433\u043e \u0442\u0438\u043f\u0430). \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0441\u043f\u0438\u0441\u043e\u043a \u0434\u0432\u0443\u0445 \u0441\u0442\u0440\u043e\u043a \u0438 \u0441\u043f\u0438\u0441\u043e\u043a \u0442\u0440\u0435\u0445 \u0441\u0442\u0440\u043e\u043a \u2014 \u044d\u0442\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u043e\u0434\u043d\u043e\u0433\u043e \u0438 \u0442\u043e\u0433\u043e \u0436\u0435 \u0442\u0438\u043f\u0430 \u2014 \u0441\u043f\u0438\u0441\u043e\u043a \u0441\u0442\u0440\u043e\u043a. \u041d\u043e \u0435\u0441\u043b\u0438 \u0432\u044b\u043d\u0435\u0441\u0442\u0438 \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044e \u043e \u0447\u0438\u0441\u043b\u0435 \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u043e\u0432 \u043d\u0430 \u0443\u0440\u043e\u0432\u0435\u043d\u044c \u0442\u0438\u043f\u0430, \u0442\u043e \u043f\u043e\u043b\u0443\u0447\u0438\u043c \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0439 \u0442\u0438\u043f \u2014 \u0432\u0435\u043a\u0442\u043e\u0440 (\u043e\u043d \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u2014 \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0447\u0438\u0441\u043b\u0430). \u0418 \u0432\u0435\u043a\u0442\u043e\u0440 \u0434\u0432\u0443\u0445 \u0441\u0442\u0440\u043e\u043a \u0438 \u0432\u0435\u043a\u0442\u043e\u0440 \u0442\u0440\u0435\u0445 \u0441\u0442\u0440\u043e\u043a \u2014 \u0440\u0430\u0437\u043d\u044b\u0435 \u0442\u0438\u043f\u044b. \u0415\u0449\u0435 \u043f\u0440\u0438\u043c\u0435\u0440\u044b \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432 \u2014 \u043d\u0435\u043d\u0443\u043b\u0435\u0432\u043e\u0435 \u0447\u0438\u0441\u043b\u043e, \u043d\u0435\u043f\u0443\u0441\u0442\u043e\u0439 \u0441\u043f\u0438\u0441\u043e\u043a, \u043f\u0430\u0440\u0430 \u0447\u0438\u0441\u0435\u043b, \u0433\u0434\u0435 \u0432\u0442\u043e\u0440\u043e\u0435 \u0447\u0438\u0441\u043b\u043e \u043c\u0435\u043d\u044c\u0448\u0435 \u043f\u0435\u0440\u0432\u043e\u0433\u043e, \u0442\u0438\u043f-\u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u043e 1 =:= 2<\/code> (\u0443 \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u043d\u0435\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439), \u0442\u0438\u043f\u044b 1 =:= 1<\/code>, 2 =:= 2<\/code> (\u0443 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u043f\u043e \u043e\u0434\u043d\u043e\u043c\u0443 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044e) \u0438 \u0442.\u0434.<\/p>\n
  \u0422\u0430\u043a \u043c\u043e\u0436\u043d\u043e \u0437\u0430\u0434\u0430\u0442\u044c \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0439 \u0442\u0438\u043f Ba<\/code>, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 \u0442\u0438\u043f\u0430 A<\/code>, \u0438 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u0443\u044e \u044d\u0442\u043e\u0433\u043e \u0442\u0438\u043f\u0430:<\/p>\n
val Ba = "B(_ : A)" :: A ->: Type val b = "b" :: Ba(a)<\/code><\/pre>\n
  <\/p>\n
\u0424\u0443\u043d\u043a\u0446\u0438\u0438<\/h4>\n
  \u0422\u0435\u043f\u0435\u0440\u044c \u043f\u0440\u043e \u0441\u0442\u0440\u0435\u043b\u043e\u0447\u043a\u0438. \u0415\u0441\u0442\u044c 4 \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0445 \u0442\u0438\u043f\u0430 \u0441\u0442\u0440\u0435\u043b\u043e\u043a \u0434\u043b\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0439: :-><\/code>, :~><\/code>, ->:<\/code>, ~>:<\/code> . \u0421 \u0434\u0432\u043e\u0435\u0442\u043e\u0447\u0438\u044f\u043c\u0438 \u0441\u043b\u0435\u0432\u0430 \u2014 \u0434\u043b\u044f \u043b\u044f\u043c\u0431\u0434 (\u0442.\u0435. \u0441\u0430\u043c\u0438\u0445 \u0444\u0443\u043d\u043a\u0446\u0438\u0439), \u0441 \u0434\u0432\u043e\u0435\u0442\u043e\u0447\u0438\u044f\u043c\u0438 \u0441\u043f\u0440\u0430\u0432\u0430 \u2014 \u0434\u043b\u044f \u0442\u0438\u043f\u043e\u0432 \u0444\u0443\u043d\u043a\u0446\u0438\u0439. \u0421 \u0434\u0435\u0444\u0438\u0441\u0430\u043c\u0438 \u2014 \u0434\u043b\u044f \u043e\u0431\u044b\u0447\u043d\u044b\u0445 \u0444\u0443\u043d\u043a\u0446\u0438\u0439, \u0441 \u0442\u0438\u043b\u044c\u0434\u0430\u043c\u0438 \u2014 \u0434\u043b\u044f \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0444\u0443\u043d\u043a\u0446\u0438\u0439 (\u0442.\u0435. \u0443 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u043d\u0435 \u0442\u043e\u043b\u044c\u043a\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435, \u043d\u043e \u0438 \u0442\u0438\u043f \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430). \u0412 \u043a\u0430\u0447\u0435\u0441\u0442\u0432\u0435 \u043f\u0440\u0438\u043c\u0435\u0440\u0430 \u2014 \u0442\u043e\u0436\u0434\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f<\/p>\n
val id = A :~> (a :-> a) !: A ~>: (A ->: A)<\/code><\/pre>\n
  \u0427\u0430\u0441\u0442\u044c \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u0442\u0438\u043f\u043e\u0432 \u043e\u0441\u0443\u0449\u0435\u0441\u0442\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0432 \u0440\u0430\u043d\u0442\u0430\u0439\u043c\u0435, \u043d\u043e \u0447\u0430\u0441\u0442\u044c \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u0438 \u043e \u0442\u0438\u043f\u0430\u0445 \u0432\u0438\u0434\u0438\u0442 \u0438 \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0442\u043e\u0440 \u0421\u043a\u0430\u043b\u044b:<\/p>\n
val f : FuncLike[Term, Term] = a :~> b !: a ~>: Ba(a) val f : Term => Term = a :~> b !: a ~>: Ba(a)<\/code><\/pre>\n
  \u0417\u0434\u0435\u0441\u044c \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u044b\u0439 \u0442\u0438\u043f \u0438\u0437 ProvingGround\/HoTT \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0442\u043e\u0440 \u0421\u043a\u0430\u043b\u044b \u0432\u0438\u0434\u0438\u0442 \u043a\u0430\u043a \u043e\u0431\u044b\u0447\u043d\u0443\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u044e \u0432 \u0421\u043a\u0430\u043b\u0435.<\/p>\n
\u0418\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0435 \u0442\u0438\u043f\u044b<\/h4>\n
  \u041c\u043e\u0436\u043d\u043e \u0437\u0430\u0434\u0430\u0432\u0430\u0442\u044c \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0435 \u0442\u0438\u043f\u044b<\/a>. \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0431\u0443\u043b\u0435\u0432 \u0442\u0438\u043f \u0441 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u0430\u043c\u0438 \u00ab\u0438\u0441\u0442\u0438\u043d\u0430\u00bb \u0438 \u00ab\u043b\u043e\u0436\u044c\u00bb:<\/p>\n
val Bool = "Boolean" :: Type val BoolInd = ("true" ::: Bool) |: ("false" ::: Bool) =: Bool val tru :: fls :: HNil = BoolInd.intros<\/code><\/pre>\n
  \u0442\u043e \u0435\u0441\u0442\u044c \u0442\u0438\u043f\u0438\u0447\u043d\u043e\u0435 \u0437\u0430\u0434\u0430\u043d\u0438\u0435 \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430 \u0432\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u043a\u0430\u043a<\/p>\n
val \u0438\u0434\u0435\u043d\u0442\u0438\u0444\u0438\u043a\u0430\u0442\u043e\u0440_\u043e\u0431\u044a\u044f\u0432\u043b\u0435\u043d\u0438\u044f = (...) |: (...) |: (...) =: \u0418\u043c\u044f_\u0442\u0438\u043f\u0430<\/code><\/pre>\n
  \u0433\u0434\u0435 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u044b \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 \u044d\u0442\u043e\u0433\u043e \u0442\u0438\u043f\u0430 \u043e\u0442\u0434\u0435\u043b\u0435\u043d\u044b |:<\/code> .<\/p>\n
  \u0415\u0449\u0435 \u043f\u0440\u0438\u043c\u0435\u0440 \u2014 \u0442\u0438\u043f \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u044b\u0445 \u0447\u0438\u0441\u0435\u043b \u0441 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u0430\u043c\u0438 \u00ab\u043d\u043e\u043b\u044c\u00bb \u0438 \u00ab\u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0435 \u0447\u0438\u0441\u043b\u043e \u0437\u0430 \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u044b\u043c n<\/code>\u00bb:<\/p>\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 \/\/ ...<\/code><\/pre>\n
  \u0422\u0438\u043f \u0446\u0435\u043b\u044b\u0445 \u0447\u0438\u0441\u0435\u043b \u0441 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u0430\u043c\u0438 \u00ab\u043f\u043b\u044e\u0441 \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u043e\u0435 n<\/code>\u00bb \u0438 \u00ab\u043c\u0438\u043d\u0443\u0441 \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u043e\u0435 n<\/code> \u043c\u0438\u043d\u0443\u0441 1\u00bb \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442 \u0443\u0436\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0439 \u0442\u0438\u043f \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u044b\u0445 \u0447\u0438\u0441\u0435\u043b:<\/p>\n
val Int = "Integer" :: Type val IntInd = ("pos" ::: Nat ->>: Int) |: ("neg" ::: Nat ->>: Int) =: Int val pos :: neg :: HNil = IntInd.intros<\/code><\/pre>\n
  \u0422\u0438\u043f \u0441\u043f\u0438\u0441\u043a\u0430 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 \u0442\u0438\u043f\u0430 A<\/code> \u0438\u043c\u0435\u0435\u0442 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u044b \u00ab\u043f\u0443\u0441\u0442\u043e\u0439 \u0441\u043f\u0438\u0441\u043e\u043a\u00bb \u0438 \u00ab\u0441\u043f\u0438\u0441\u043e\u043a \u0441 \u0433\u043e\u043b\u043e\u0432\u043e\u0439 \u0442\u0438\u043f\u0430 A<\/code> \u0438 \u0445\u0432\u043e\u0441\u0442\u043e\u043c \u0442\u0438\u043f\u0430 ListA<\/code>\u00bb:<\/p>\n
val ListA = "List(A)" :: Type val ListAInd = ("nil" ::: ListA) |: ("cons" ::: A ->>: ListA -->>: ListA) =: ListA val nil :: cons :: HNil = ListAInd.intros<\/code><\/pre>\n
  \u0423 \u0442\u0438\u043f\u0430 \u0431\u0438\u043d\u0430\u0440\u043d\u043e\u0433\u043e \u0434\u0435\u0440\u0435\u0432\u0430 (\u0434\u043b\u044f \u043f\u0440\u043e\u0441\u0442\u043e\u0442\u044b \u0431\u0435\u0437 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u0442\u0438\u043f\u0430 \u0432 \u0443\u0437\u043b\u0430\u0445) \u0435\u0441\u0442\u044c \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u044b \u00ab\u043b\u0438\u0441\u0442\u00bb \u0438 \u00ab\u0432\u0438\u043b\u043a\u0430\u00bb (\u0432\u0442\u043e\u0440\u043e\u0439 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u043f\u0430\u0440\u0443 \u043f\u043e\u0434\u0434\u0435\u0440\u0435\u0432\u044c\u0435\u0432):<\/p>\n
val BTree = "BTree" :: Type val BTreeInd = ("leaf" ::: BTree) |: ("fork" ::: BTree -->>: BTree -->>: BTree) =: BTree val leaf :: fork :: HNil = BTreeInd.intros<\/code><\/pre>\n
  \u0410\u043b\u044c\u0442\u0435\u0440\u043d\u0430\u0442\u0438\u0432\u043d\u043e \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 \u00ab\u0432\u0438\u043b\u043a\u0430\u00bb \u043c\u043e\u0433\u043b\u0430 \u0431\u044b \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0442\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u044e, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043f\u0435\u0440\u0435\u0432\u043e\u0434\u0438\u0442 \u043b\u043e\u0436\u044c \u0432 \u043e\u0434\u043d\u043e \u043f\u043e\u0434\u0434\u0435\u0440\u0435\u0432\u043e, \u0438\u0441\u0442\u0438\u043d\u0443 \u0432 \u0434\u0440\u0443\u0433\u043e\u0435:<\/p>\n
val BTree = "BTree" :: Type val BTreeInd = ("leaf" ::: BTree) |: ("fork" ::: (Bool -|>: BTree) -->>: BTree) =: BTree val leaf :: fork :: HNil = BTreeInd.intros<\/code><\/pre>\n
  <\/p>\n
\u0417\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0435 \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0435 \u0442\u0438\u043f\u044b<\/h4>\n
  \u0415\u0441\u043b\u0438 \u0442\u0438\u043f \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0439 (indexed inductive type<\/a>), \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440 \u0432\u0435\u043a\u0442\u043e\u0440 Vec<\/code> \u0438\u043b\u0438 \u0442\u0438\u043f-\u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u043e Id<\/code>, \u0442\u043e \u043d\u0430\u0434\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c =::<\/code> \u0432\u043c\u0435\u0441\u0442\u043e =:<\/code>, \u0441\u0442\u0440\u0435\u043b\u043a\u0443 \u0441 \u0442\u0438\u043b\u044c\u0434\u043e\u0439 \u0438 \u0441\u0441\u044b\u043b\u0430\u0442\u044c\u0441\u044f \u043d\u0430 \u0442\u0438\u043f \u0432\u043d\u0443\u0442\u0440\u0438 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u043e\u0432 (\u0418\u043c\u044f_\u0442\u0438\u043f\u0430 -> \u0418\u043c\u044f_\u0442\u0438\u043f\u0430(n))<\/code> \u0432 \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u043c\u043e\u043c \u0442\u0438\u043f\u0435, (\u0418\u043c\u044f_\u0442\u0438\u043f\u0430 :> \u0418\u043c\u044f_\u0442\u0438\u043f\u0430(n))<\/code> \u0432 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u043c\u043e\u043c \u0442\u0438\u043f\u0435, \u0430 \u043d\u0435 \u043f\u0440\u043e\u0441\u0442\u043e \u0418\u043c\u044f_\u0442\u0438\u043f\u0430(n)<\/code>. \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0442\u0438\u043f \u0432\u0435\u043a\u0442\u043e\u0440\u0430 \u0434\u043b\u0438\u043d\u044b n<\/code>:<\/p>\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<\/code><\/pre>\n
  \u0415\u0449\u0435 \u043e\u0434\u0438\u043d \u043f\u043e\u043b\u0435\u0437\u043d\u044b\u0439 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0439 \u0442\u0438\u043f \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0444\u043e\u0440\u043c\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u0442\u044c \u043f\u043e\u043d\u044f\u0442\u0438\u0435 \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0447\u0438\u0441\u043b\u0430, \u043d\u0435 \u043f\u0440\u0435\u0432\u044b\u0448\u0430\u044e\u0449\u0435\u0433\u043e \u0434\u0440\u0443\u0433\u043e\u0435 \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u043e\u0435 \u0447\u0438\u0441\u043b\u043e:<\/p>\n
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<\/code><\/pre>\n
  \u0414\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e, \u043d\u0435\u0442 \u0441\u043f\u043e\u0441\u043e\u0431\u0430 \u0441\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 Fin(zero)<\/code>. \u0415\u0441\u0442\u044c \u0440\u043e\u0432\u043d\u043e \u043e\u0434\u043d\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 Fin(one)<\/code>:<\/p>\n
val fz0 = fz(zero) !: Fin(one)<\/code><\/pre>\n
  \u0415\u0441\u0442\u044c \u0440\u043e\u0432\u043d\u043e \u0434\u0432\u0430 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0442\u0438\u043f\u0430 Fin(two)<\/code>:<\/p>\n
val fz1 = fz(one) !: Fin(two) val fs1 = fs(one)(fz0) !: Fin(two)<\/code><\/pre>\n
  \u0415\u0441\u0442\u044c \u0440\u043e\u0432\u043d\u043e \u0442\u0440\u0438 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0442\u0438\u043f\u0430 Fin(three)<\/code>:<\/p>\n
fz(two) !: Fin(three) fs(two)(fz1) !: Fin(three) fs(two)(fs1) !: Fin(three)<\/code><\/pre>\n
  \u0438 \u0442.\u0434.<\/p>\n
\u0421\u0435\u043c\u0435\u0439\u0441\u0442\u0432\u0430 \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0445 \u0442\u0438\u043f\u043e\u0432<\/h4>\n
  \u041d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0441\u043b\u043e\u0432 \u043e\u0431 \u043e\u0442\u043b\u0438\u0447\u0438\u0438 \u0441\u0435\u043c\u0435\u0439\u0441\u0442\u0432\u0430 \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0445 \u0442\u0438\u043f\u043e\u0432 (family of inductive types) \u043e\u0442 \u0438\u043d\u0434\u0435\u043a\u0441\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u0433\u043e \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430 (indexed inductive type). \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, List(A)<\/code> \u2014 \u044d\u0442\u043e \u0441\u0435\u043c\u0435\u0439\u0441\u0442\u0432\u043e, \u0430 Vec(A)(n)<\/code> \u2014 \u044d\u0442\u043e \u0441\u0435\u043c\u0435\u0439\u0441\u0442\u0432\u043e \u043e\u0442\u043d\u043e\u0441\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0442\u0438\u043f\u0430 A<\/code>, \u043d\u043e \u0438\u043d\u0434\u0435\u043a\u0441\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0439 \u0442\u0438\u043f \u043e\u0442\u043d\u043e\u0441\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0438\u043d\u0434\u0435\u043a\u0441\u0430 n<\/code>. \u0418\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0439 \u0442\u0438\u043f \u2014 \u044d\u0442\u043e \u0442\u0438\u043f, \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u044b \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u0434\u043b\u044f \u00ab\u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0445\u00bb \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 \u043c\u043e\u0433\u0443\u0442 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u00ab\u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0438\u0435\u00bb \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f (\u043a\u0430\u043a \u0443 \u0442\u0438\u043f\u043e\u0432 Nat<\/code>, List<\/code> \u0438 \u0442.\u0434.). Vec(A)(n)<\/code> \u043f\u0440\u0438 \u0444\u0438\u043a\u0441\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u043c A<\/code> \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u043c \u0442\u0438\u043f\u043e\u043c, \u043d\u043e \u043d\u0435 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043f\u0440\u0438 \u0444\u0438\u043a\u0441\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u043c n<\/code>. \u0412 ProvingGround \u0432 \u043d\u0430\u0441\u0442\u043e\u044f\u0449\u0435\u0435 \u0432\u0440\u0435\u043c\u044f \u043d\u0435\u0442 \u0441\u0435\u043c\u0435\u0439\u0441\u0442\u0432 \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0445 \u0442\u0438\u043f\u043e\u0432, \u0442.\u0435. \u043d\u0435\u043b\u044c\u0437\u044f, \u0438\u043c\u0435\u044f \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0442\u0438\u043f\u0430 List(A)<\/code>, \u043b\u0435\u0433\u043a\u043e \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u043e\u0432 List(B)<\/code>, List(Nat)<\/code>, List(Bool)<\/code>, List(List(A))<\/code> \u0438 \u0442.\u0434. \u041d\u043e \u043c\u043e\u0436\u043d\u043e \u044d\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0441\u0435\u043c\u0435\u0439\u0441\u0442\u0432\u0430 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0438\u043d\u0434\u0435\u043a\u0441\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0445 \u0442\u0438\u043f\u043e\u0432:<\/p>\n
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)  \/\/ \u0441\u043f\u0438\u0441\u043e\u043a 0, 1, 2<\/code><\/pre>\n
  \u0438<\/p>\n
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-\u044d\u043b\u0435\u043c\u0435\u043d\u0442\u043d\u044b\u0439 \u0432\u0435\u043a\u0442\u043e\u0440 tru, fls, tru<\/code><\/pre>\n
  \u041c\u043e\u0436\u043d\u043e \u0442\u0430\u043a\u0436\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u0433\u0435\u0442\u0435\u0440\u043e\u0433\u0435\u043d\u043d\u044b\u0439 \u0441\u043f\u0438\u0441\u043e\u043a (HList<\/code>):<\/p>\n
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<\/code><\/pre>\n
  \u041c\u044b \u0441\u0435\u0439\u0447\u0430\u0441 \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043b\u0438 \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u044b\u0439 HList<\/code> \u0432 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435 ProvingGround, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u0430 \u043f\u043e\u0432\u0435\u0440\u0445 Shapeless, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u043c \u0441\u0442\u0440\u043e\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u043c \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u043e\u043c \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f HList<\/code>.<\/p>\n
\u0410\u043b\u0433\u0435\u0431\u0440\u0430\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u0442\u0438\u043f\u044b \u0434\u0430\u043d\u043d\u044b\u0445<\/h4>\n
  \u0412 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435 \u043c\u043e\u0436\u043d\u043e \u044d\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043e\u0431\u043e\u0431\u0449\u0435\u043d\u043d\u044b\u0435 \u0430\u043b\u0433\u0435\u0431\u0440\u0430\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u0442\u0438\u043f\u044b \u0434\u0430\u043d\u043d\u044b\u0445 (GADT<\/a>). \u041a\u043e\u0434, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0432\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u043d\u0430 \u0425\u0430\u0441\u043a\u0435\u043b\u0435<\/p>\n
{-# 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<\/code><\/pre>\n
  \u0438 \u043d\u0430 \u0447\u0438\u0441\u0442\u043e\u0439 \u0421\u043a\u0430\u043b\u0435<\/p>\n
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]<\/code><\/pre>\n
  \u0437\u0430\u043f\u0438\u0448\u0435\u0442\u0441\u044f \u0432 ProvingGround \u043a\u0430\u043a<\/p>\n
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<\/code><\/pre>\n
  <\/p>\n
\u041a\u043b\u0430\u0441\u0441\u044b \u0442\u0438\u043f\u043e\u0432<\/h4>\n
  \u0422\u0430\u043a\u0436\u0435 \u043c\u043e\u0436\u043d\u043e \u0432 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435 \u044d\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043a\u043b\u0430\u0441\u0441\u044b \u0442\u0438\u043f\u043e\u0432<\/a>. \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0444\u0443\u043d\u043a\u0442\u043e\u0440<\/a>:<\/p>\n
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<\/code><\/pre>\n
  \u041c\u043e\u0436\u043d\u043e, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0441\u043f\u0438\u0441\u043e\u043a \u043e\u0431\u044a\u044f\u0432\u0438\u0442\u044c \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440\u043e\u043c (instance) \u0444\u0443\u043d\u043a\u0442\u043e\u0440\u0430:<\/p>\n
val as = "as" :: List(A) val indList_map = ListInd.induc(A :~> (as :-> (B ~>: ((A ->: B) ->: List(B) )))) \/\/ \u044d\u0442\u043e \u0438\u043d\u0434\u0443\u043a\u0446\u0438\u044f, \u043e \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0438 \u0438 \u0438\u043d\u0434\u0443\u043a\u0446\u0438\u0438 \u0438\u0434\u0435\u0442 \u0440\u0435\u0447\u044c \u043d\u0438\u0436\u0435 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)<\/code><\/pre>\n
  \u041c\u043e\u0436\u043d\u043e \u0432 \u043a\u043b\u0430\u0441\u0441 \u0442\u0438\u043f\u043e\u0432 \u0434\u043e\u0431\u0430\u0432\u0438\u0442\u044c \u0437\u0430\u043a\u043e\u043d\u044b:<\/p>\n
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<\/code><\/pre>\n
  <\/p>\n
\u0422\u0438\u043f\u044b-\u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u0430<\/h4>\n
  \u0412 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435 \u0443\u0436\u0435 \u0435\u0441\u0442\u044c \u0432\u0441\u0442\u0440\u043e\u0435\u043d\u043d\u044b\u0435 \u0441\u0438\u0433\u043c\u0430-\u0442\u0438\u043f (\u0442\u0438\u043f \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0439 \u043f\u0430\u0440\u044b), \u043f\u0438-\u0442\u0438\u043f (\u0442\u0438\u043f \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438, \u043c\u044b \u0435\u0433\u043e \u0443\u0436\u0435 \u0432\u0438\u0434\u0435\u043b\u0438 \u0432\u044b\u0448\u0435), \u0442\u0438\u043f-\u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u043e (identity type):<\/p>\n
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<\/code><\/pre>\n
  \u043d\u043e \u043c\u043e\u0436\u043d\u043e \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u0438 \u0441\u0432\u043e\u0439, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0442\u0438\u043f-\u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u043e:<\/p>\n
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)<\/code><\/pre>\n
  \u0422\u0438\u043f\u044b-\u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u0430 \u0435\u0441\u0442\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u043e \u0432\u043e\u0437\u043d\u0438\u043a\u0430\u044e\u0442, \u043a\u043e\u0433\u0434\u0430 \u043d\u0430\u0447\u0438\u043d\u0430\u0435\u0442\u0441\u044f \u0440\u0430\u0437\u0433\u043e\u0432\u043e\u0440 \u043e \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0438\u0438 \u041a\u0430\u0440\u0440\u0438-\u0425\u043e\u0432\u0430\u0440\u0434\u0430<\/a>. \u0421 \u043e\u0434\u043d\u043e\u0439 \u0441\u0442\u043e\u0440\u043e\u043d\u044b A ->: B<\/code> \u2014 \u044d\u0442\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0438\u0437 A<\/code> \u0432 B<\/code>, \u0441 \u0434\u0440\u0443\u0433\u043e\u0439 \u2014 \u044d\u0442\u043e \u043b\u043e\u0433\u0438\u0447\u0435\u0441\u043a\u0430\u044f \u0444\u043e\u0440\u043c\u0443\u043b\u0430 \u00ab\u0438\u0437 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u044f A<\/code> \u0441\u043b\u0435\u0434\u0443\u0435\u0442 B<\/code>\u00bb. \u0418, \u0441 \u043e\u0434\u043d\u043e\u0439 \u0441\u0442\u043e\u0440\u043e\u043d\u044b, (A ->: B) ->: A ->: B<\/code> \u2014 \u044d\u0442\u043e \u0442\u0438\u043f \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0432\u044b\u0441\u0448\u0435\u0433\u043e \u043f\u043e\u0440\u044f\u0434\u043a\u0430, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u043d\u0430 \u0432\u0445\u043e\u0434 \u0444\u0443\u043d\u043a\u0446\u0438\u044e A ->: B<\/code> \u0438 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 A<\/code> \u0438 \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u044d\u0442\u0443 \u0444\u0443\u043d\u043a\u0446\u0438\u044e, \u043f\u0440\u0438\u043c\u0435\u043d\u0435\u043d\u043d\u0443\u044e \u043a \u044d\u0442\u043e\u043c\u0443 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044e, \u0442.\u0435. \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 B<\/code>. \u0421 \u0434\u0440\u0443\u0433\u043e\u0439 \u0441\u0442\u043e\u0440\u043e\u043d\u044b, \u044d\u0442\u043e \u043f\u0440\u0430\u0432\u0438\u043b\u043e \u0432\u044b\u0432\u043e\u0434\u0430 \u0432 \u043b\u043e\u0433\u0438\u043a\u0435 modus ponens \u2014 \u00ab\u0435\u0441\u043b\u0438 \u0432\u0435\u0440\u043d\u043e, \u0447\u0442\u043e \u0438\u0437 A<\/code> \u0441\u043b\u0435\u0434\u0443\u0435\u0442 B<\/code>, \u0438 \u0432\u0435\u0440\u043d\u043e A<\/code>, \u0442\u043e \u0432\u0435\u0440\u043d\u043e B<\/code>\u00bb. \u0421 \u0442\u0430\u043a\u043e\u0439 \u0442\u043e\u0447\u043a\u0438 \u0437\u0440\u0435\u043d\u0438\u044f \u0442\u0438\u043f\u044b \u2014 \u044d\u0442\u043e \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u044f, \u0430 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0442\u0438\u043f\u043e\u0432 \u2014 \u044d\u0442\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u044d\u0442\u0438\u0445 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u0439. \u0418 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u0435 \u0432\u0435\u0440\u043d\u043e, \u0435\u0441\u043b\u0438 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u044e\u0449\u0438\u0439 \u0442\u0438\u043f \u043d\u0430\u0441\u0435\u043b\u0435\u043d, \u0442.\u0435. \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u044d\u0442\u043e\u0433\u043e \u0442\u0438\u043f\u0430. \u041b\u043e\u0433\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u00ab\u0438\u00bb \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u043f\u0440\u043e\u0438\u0437\u0432\u0435\u0434\u0435\u043d\u0438\u044e \u0442\u0438\u043f\u043e\u0432, \u043b\u043e\u0433\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u00ab\u0438\u043b\u0438\u00bb \u2014 \u0441\u0443\u043c\u043c\u0435 \u0442\u0438\u043f\u043e\u0432, \u043b\u043e\u0433\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u00ab\u043d\u0435\u00bb \u2014 \u0442\u0438\u043f\u0443 A ->: Zero<\/code>, \u0442.\u0435. \u0444\u0443\u043d\u043a\u0446\u0438\u044f\u043c \u0432 \u043f\u0443\u0441\u0442\u043e\u0439 \u0442\u0438\u043f. \u0422\u0430\u043a \u0432 \u0442\u0435\u043e\u0440\u0438\u0438 \u0442\u0438\u043f\u043e\u0432 \u0432\u043e\u0437\u043d\u0438\u043a\u0430\u0435\u0442 \u043b\u043e\u0433\u0438\u043a\u0430. \u041f\u0440\u0430\u0432\u0434\u0430, \u043d\u0435 \u043b\u044e\u0431\u0430\u044f \u043b\u043e\u0433\u0438\u043a\u0430, \u0430 \u0442\u0430\u043a \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u043c\u0430\u044f \u0438\u043d\u0442\u0443\u0438\u0446\u0438\u043e\u043d\u0438\u0441\u0442\u0441\u043a\u0430\u044f<\/a> \u0438\u043b\u0438 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u0438\u0432\u043d\u0430\u044f, \u0442.\u0435. \u043b\u043e\u0433\u0438\u043a\u0430 \u0431\u0435\u0437 \u0437\u0430\u043a\u043e\u043d\u0430 \u0438\u0441\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u044f \u0442\u0440\u0435\u0442\u044c\u0435\u0433\u043e. \u0414\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e, \u0432\u043e\u043e\u0431\u0449\u0435 \u0433\u043e\u0432\u043e\u0440\u044f, \u043d\u0435\u043b\u044c\u0437\u044f \u0441\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 PlusTyp(A, A ->: Zero)<\/code> (\u0435\u0441\u043b\u0438 \u043d\u0435 \u0443\u0434\u0430\u043b\u043e\u0441\u044c \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c A<\/code>, \u0442\u043e \u044d\u0442\u043e \u0435\u0449\u0435 \u043d\u0435 \u0437\u043d\u0430\u0447\u0438\u0442, \u0447\u0442\u043e \u0443\u0434\u0430\u043b\u043e\u0441\u044c \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u043d\u0435-A<\/code>). \u0418\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u043e, \u0447\u0442\u043e \u0441\u043f\u0440\u0430\u0432\u0435\u0434\u043b\u0438\u0432\u043e \u043e\u0442\u0440\u0438\u0446\u0430\u043d\u0438\u0435 \u043a \u043e\u0442\u0440\u0438\u0446\u0430\u043d\u0438\u044e \u0437\u0430\u043a\u043e\u043d\u0430 \u0438\u0441\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u044f \u0442\u0440\u0435\u0442\u044c\u0435\u0433\u043e:<\/p>\n
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<\/code><\/pre>\n
  \u041d\u0443 \u0442\u0430\u043a \u0432\u043e\u0442, \u0435\u0441\u043b\u0438 \u0442\u0438\u043f\u044b \u2014 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u044f, \u0430 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0442\u0438\u043f\u043e\u0432 \u2014 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430, \u0442\u043e \u0440\u0430\u0437 \u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u043e \u0434\u0432\u0443\u0445 \u0442\u0435\u0440\u043c\u043e\u0432 a1 =:= a2<\/code> \u2014 \u044d\u0442\u043e \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u0435, \u0437\u043d\u0430\u0447\u0438\u0442 \u0438 \u0442\u0438\u043f. \u0422\u0438\u043f \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0439, \u0442.\u043a. \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 a1, a2<\/code> \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u0442\u0438\u043f\u0430 A<\/code>. \u0415\u0441\u043b\u0438 a1, a2<\/code> \u0440\u0430\u0437\u043d\u044b\u0435, \u0442\u043e \u043d\u0435 \u0434\u043e\u043b\u0436\u043d\u043e \u0431\u044b\u0442\u044c \u0441\u043f\u043e\u0441\u043e\u0431\u0430 \u0441\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u044d\u0442\u043e\u0433\u043e \u0442\u0438\u043f\u0430, \u0442.\u043a. \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u0435 \u043b\u043e\u0436\u043d\u043e. \u0415\u0441\u043b\u0438 \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u044b\u0435, \u0442\u043e \u043d\u0430\u043e\u0431\u043e\u0440\u043e\u0442 \u0434\u043e\u043b\u0436\u0435\u043d \u0431\u044b\u0442\u044c \u0441\u043f\u043e\u0441\u043e\u0431 \u0441\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435, \u0440\u0430\u0437 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u0435 \u0432\u0435\u0440\u043d\u043e, \u0442\u0430\u043a \u0447\u0442\u043e \u0443 \u043d\u0430\u0448\u0435\u0433\u043e \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430 \u0435\u0434\u0438\u043d\u0441\u0442\u0432\u0435\u043d\u043d\u044b\u0439 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 refl(A)(a) !: Id(A)(a)(a)<\/code> (\u0438\u043b\u0438 a.refl !: (a =:= a)<\/code> \u0434\u043b\u044f \u0432\u0441\u0442\u0440\u043e\u0435\u043d\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430-\u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u0430).<\/p>\n
  \u0415\u0449\u0435 \u043e\u0434\u0438\u043d \u043f\u043e\u043b\u0435\u0437\u043d\u044b\u0439 \u0442\u0438\u043f \u043f\u0440\u0438 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0435 \u0442\u0435\u043e\u0440\u0435\u043c \u0441 \u043d\u0435\u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u0430\u043c\u0438:<\/p>\n
val LTE = "\u2264" :: Nat ->: Nat ->: Type val LTEInd = {"0 \u2264 _" ::: m ~>>: (LTE -> LTE(zero)(m) )} |:      {"S _ \u2264 S _" ::: n ~>>: m ~>>: ((LTE :> LTE(n)(m) ) -->>: (LTE -> LTE(succ(n))(succ(m)) ))} =:: LTE val lteZero :: lteSucc :: HNil = LTEInd.intros<\/code><\/pre>\n
  <\/p>\n
\u0412\u044b\u0441\u0448\u0438\u0435 \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0435 \u0442\u0438\u043f\u044b<\/h4>\n
  \u0415\u0449\u0435 \u0432 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435 \u043c\u043e\u0436\u043d\u043e \u0440\u0430\u0431\u043e\u0442\u0430\u0442\u044c \u0441 \u0432\u044b\u0441\u0448\u0438\u043c\u0438 \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u043c\u0438 \u0442\u0438\u043f\u0430\u043c\u0438<\/a>. \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u043e\u043a\u0440\u0443\u0436\u043d\u043e\u0441\u0442\u044c\u044e<\/p>\n
val Circle = "S^1" :: Type val base = "base" :: Circle \/\/ \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 val loop = "loop" :: (base =:= base) \/\/ \u0435\u0449\u0435 \u043e\u0434\u0438\u043d \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440<\/code><\/pre>\n
  \u0438 \u0441\u0444\u0435\u0440\u043e\u0439<\/p>\n
val Sphere = "S^2" :: Type val base = "base" :: Sphere \/\/ \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 val surf = "surf" :: (base.refl =:= base.refl) \/\/ \u0435\u0449\u0435 \u043e\u0434\u0438\u043d \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 \/\/  val surf = "surf" :: IdentityTyp(base =:= base, base.refl, base.refl) \/\/  val surf = "surf" :: IdentityTyp(IdentityTyp(Sphere, base, base), base.refl, base.refl)<\/code><\/pre>\n
  <\/p>\n
\u0420\u0435\u043a\u0443\u0440\u0441\u0438\u044f \u0438 \u0438\u043d\u0434\u0443\u043a\u0446\u0438\u044f<\/h4>\n
  \u0422\u0435\u043f\u0435\u0440\u044c \u043e \u0442\u043e\u043c, \u043a\u0430\u043a \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0442\u044c (\u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0432\u043d\u044b\u0435) \u0444\u0443\u043d\u043a\u0446\u0438\u0438. \u0411\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 \u0434\u043b\u044f \u043a\u0430\u0436\u0434\u043e\u0433\u043e \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430 \u0433\u0435\u043d\u0435\u0440\u0438\u0440\u0443\u0435\u0442 \u043c\u0435\u0442\u043e\u0434\u044b .rec<\/code>, .induc<\/code>, \u0442.\u0435. \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u044e (aka \u0440\u0435\u043a\u0443\u0440\u0441\u043e\u0440) \u0438 \u0438\u043d\u0434\u0443\u043a\u0446\u0438\u044e \u2014 \u044d\u043b\u0438\u043c\u0438\u043d\u0430\u0442\u043e\u0440\u044b \u0432 \u043f\u043e\u0441\u0442\u043e\u044f\u043d\u043d\u044b\u0439 \u0438 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0439 \u0442\u0438\u043f \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0435\u043d\u043d\u043e, \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u043c\u043e\u0436\u043d\u043e \u043e\u0441\u0443\u0449\u0435\u0441\u0442\u0432\u043b\u044f\u0442\u044c \u0441\u043e\u043f\u043e\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u0441 \u043e\u0431\u0440\u0430\u0437\u0446\u043e\u043c (pattern matching), \u0435\u0441\u043b\u0438 \u043d\u0430\u0434\u043e \u2014 \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0432\u043d\u043e\u0435. \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u043c\u043e\u0436\u043d\u043e \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u043b\u043e\u0433\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u00ab\u043d\u0435\u00bb:<\/p>\n
val b = "b" :: Bool val recBB = BoolInd.rec(Bool) val not = recBB(fls)(tru)<\/code><\/pre>\n
  \u0417\u0434\u0435\u0441\u044c \u043c\u043e\u0436\u043d\u043e \u0441\u0447\u0438\u0442\u0430\u0442\u044c, \u0447\u0442\u043e \u043c\u044b \u0441\u0434\u0435\u043b\u0430\u043b\u0438 \u0441\u043e\u043f\u043e\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u0441 \u043e\u0431\u0440\u0430\u0437\u0446\u043e\u043c:<\/p>\n
match {   case true => false   case false => true }<\/code><\/pre>\n
  \u041f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c, \u0447\u0442\u043e \u0432\u0441\u0451 \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442:<\/p>\n
not(tru) == fls not(fls) == tru<\/code><\/pre>\n
  \u0422\u0430\u043a\u0436\u0435 \u043c\u043e\u0436\u043d\u043e \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u043b\u043e\u0433\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u00ab\u0438\u00bb:<\/p>\n
val recBBB = BoolInd.rec(Bool ->: Bool) val and = recBBB(b :-> b)(b :-> fls)<\/code><\/pre>\n
  \u0417\u0434\u0435\u0441\u044c \u043c\u043e\u0436\u043d\u043e \u0441\u0447\u0438\u0442\u0430\u0442\u044c, \u0447\u0442\u043e \u043c\u044b \u0441\u0434\u0435\u043b\u0430\u043b\u0438 \u0441\u043e\u043f\u043e\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u0441 \u043e\u0431\u0440\u0430\u0437\u0446\u043e\u043c \u043f\u043e \u043f\u0435\u0440\u0432\u043e\u043c\u0443 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0443:<\/p>\n
\/\/ \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434 match {   case true => (b => b)   case false => (b => false) }<\/code><\/pre>\n
  \u041f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c:<\/p>\n
and(fls)(tru) == fls and(tru)(tru) == tru<\/code><\/pre>\n
  \u041c\u043e\u0436\u043d\u043e \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u0443\u0434\u0432\u0430\u0438\u0432\u0430\u043d\u0438\u0435 \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0447\u0438\u0441\u043b\u0430:<\/p>\n
val n = "n" :: Nat val m = "m" :: Nat val recNN = NatInd.rec(Nat) val double = recNN(zero)(n :-> (m :-> succ(succ(m)) ))<\/code><\/pre>\n
  \u0417\u0434\u0435\u0441\u044c \u043e\u043f\u044f\u0442\u044c \u043c\u043e\u0436\u043d\u043e \u0441\u0447\u0438\u0442\u0430\u0442\u044c, \u0447\u0442\u043e \u043c\u044b \u0441\u0434\u0435\u043b\u0430\u043b\u0438 \u0441\u043e\u043f\u043e\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u0441 \u043e\u0431\u0440\u0430\u0437\u0446\u043e\u043c:<\/p>\n
\/\/ \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434 match {   case Zero => Zero   case Succ(n) =>     val m = double(n)     m + 2 }<\/code><\/pre>\n
  \u041f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c:<\/p>\n
println(double(two).fansi) > succ(succ(succ(succ(0))))<\/code><\/pre>\n
  \u041e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u043c \u0441\u043b\u043e\u0436\u0435\u043d\u0438\u0435 \u043d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u044b\u0445 \u0447\u0438\u0441\u0435\u043b:<\/p>\n
val recNNN = NatInd.rec(Nat ->: Nat) val addn = "add(n)" :: Nat ->: Nat val add = recNNN(m :-> m)(n :-> (addn :-> (m :-> succ(addn(m)) )))<\/code><\/pre>\n
  \u0417\u0434\u0435\u0441\u044c \u0430\u043d\u0430\u043b\u043e\u0433\u0438\u0447\u043d\u043e \u043c\u043e\u0436\u043d\u043e \u0441\u0447\u0438\u0442\u0430\u0442\u044c, \u0447\u0442\u043e \u043c\u044b \u0441\u0434\u0435\u043b\u0430\u043b\u0438 \u0441\u043e\u043f\u043e\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u0441 \u043e\u0431\u0440\u0430\u0437\u0446\u043e\u043c \u043f\u043e \u043f\u0435\u0440\u0432\u043e\u043c\u0443 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0443:<\/p>\n
\/\/ \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434 match {   case Zero => (m => m)   case Succ(n) =>     val addn = add(n)     m => addn(m) + 1 }<\/code><\/pre>\n
  \u041f\u0440\u043e\u0432\u0435\u0440\u043a\u0430:<\/p>\n
println(add(two)(three).fansi) > succ(succ(succ(succ(succ(0)))))<\/code><\/pre>\n
  \u041e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u043c \u0442\u0430\u043a\u0436\u0435 \u043a\u043e\u043d\u043a\u0430\u0442\u0435\u043d\u0430\u0446\u0438\u044e \u0432\u0435\u043a\u0442\u043e\u0440\u043e\u0432:<\/p>\n
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)) ))))))<\/code><\/pre>\n
  \u0417\u0434\u0435\u0441\u044c \u043c\u044b \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c \u043d\u0435 \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u044e, \u0430 \u0438\u043d\u0434\u0443\u043a\u0446\u0438\u044e, \u0442.\u043a. \u043d\u0430\u043c \u043d\u0443\u0436\u0435\u043d \u044d\u043b\u0438\u043c\u0438\u043d\u0430\u0442\u043e\u0440 \u0432 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0439 \u0442\u0438\u043f 
  m ~>: (VecA(m) ->: VecA(add(n)(m)))<\/code> \u2014 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e, \u044d\u0442\u043e\u0442 \u0442\u0438\u043f \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442 n<\/code> \u0438\u0437 \u0432\u0435\u043a\u0442\u043e\u0440\u0430 (\u043f\u0435\u0440\u0432\u044b\u0439 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442 \u043a\u043e\u043d\u043a\u0430\u0442\u0435\u043d\u0430\u0446\u0438\u0438), \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043c\u044b \u0434\u0435\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u0443\u0435\u043c \u043f\u0440\u0438 \u0441\u043e\u043f\u043e\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0438 \u0441 \u043e\u0431\u0440\u0430\u0437\u0446\u043e\u043c:<\/p>\n
\/\/ \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434 match {   case (Zero, Nil) => (vm => vm)   case (Succ(n), Cons(a)(vn)) =>     val concatVn = concat(vn)     vm => Cons(a)(concatVn(vm)) }<\/code><\/pre>\n
  \u0422\u0435\u0441\u0442\u0438\u0440\u0443\u0435\u043c:<\/p>\n
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)))))<\/code><\/pre>\n
  \u041f\u043e\u043a\u0430\u0436\u0443 \u0435\u0449\u0435 \u043f\u0440\u0438\u043c\u0435\u0440, \u043a\u0430\u043a \u0442\u0435\u043e\u0440\u0435\u043c\u044b \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u044e\u0442\u0441\u044f \u0432 ProvingGround. \u0414\u043e\u043a\u0430\u0436\u0435\u043c, \u0447\u0442\u043e add(n)(n) =:= double(n)<\/code>.<\/p>\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) )<\/code><\/pre>\n
  \u041e\u043a\u0440\u0443\u0436\u043d\u043e\u0441\u0442\u044c \u043d\u0435 \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442\u0441\u044f \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u043a\u0430\u043a \u043e\u0431\u044b\u0447\u043d\u044b\u0439 \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0439 \u0442\u0438\u043f \u0447\u0435\u0440\u0435\u0437 (...) |: (...) =:: ...<\/code> (\u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e, \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 loop<\/code> \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u043d\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 Circle<\/code>, \u043a\u0430\u043a \u0431\u044b\u043b\u043e \u0431\u044b \u0434\u043b\u044f \u043e\u0431\u044b\u0447\u043d\u043e\u0433\u043e \u0438\u043d\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430). \u041f\u043e\u044d\u0442\u043e\u043c\u0443 \u0438 \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u044e \u0441 \u0438\u043d\u0434\u0443\u043a\u0446\u0438\u0435\u0439 \u043f\u0440\u0438\u0445\u043e\u0434\u0438\u0442\u0441\u044f \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0442\u044c \u0432\u0440\u0443\u0447\u043d\u0443\u044e:<\/p>\n
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) )<\/code><\/pre>\n
  \u0441 \u0434\u0432\u0443\u043c\u044f \u0430\u043a\u0441\u0438\u043e\u043c\u0430\u043c\u0438 comp_base<\/code> \u0438 comp_loop<\/code>:<\/p>\n
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 \u0430\u043d\u0430\u043b\u043e\u0433\u0438\u0447\u043d\u043e IdentityTyp.extnslty(f), \u043d\u043e \u0434\u043b\u044f \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0439 f val comp_loop = "comp_loop" :: B ~>: b ~>: l ~>: ( dep_map(Circle)(B)(indCirc(B)(b)(l))(base)(base)(loop) =:= l )<\/code><\/pre>\n
  \u041d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0441\u043b\u043e\u0432 \u043e \u0442\u043e\u043c, \u043a\u0430\u043a \u0437\u0430\u043f\u0443\u0441\u043a\u0430\u0442\u044c \u043a\u043e\u0434 \u043d\u0430 ProvingGround. \u0415\u0441\u0442\u044c 3 \u0441\u043f\u043e\u0441\u043e\u0431\u0430.<\/p>\n
    \n
  1. \u041f\u0435\u0440\u0432\u044b\u0439 \u0438 \u0440\u0435\u043a\u043e\u043c\u0435\u043d\u0434\u0443\u0435\u043c\u044b\u0439 \u2014 \u0438\u0437 \u043a\u043e\u043d\u0441\u043e\u043b\u0438 (\u0437\u0430\u0433\u0440\u0443\u0436\u0430\u0435\u0442\u0441\u044f Ammonite REPL<\/a>) \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043a\u043e\u043c\u0430\u043d\u0434\u044b 
          sbt<\/a> mantle\/test:run<\/b> (\u0438\u0437 \u043a\u043e\u0440\u043d\u044f \u043f\u0440\u043e\u0435\u043a\u0442\u0430 ProvingGround \u043f\u043e\u0441\u043b\u0435 \u043a\u043b\u043e\u043d\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0440\u0435\u043f\u043e\u0437\u0438\u0442\u043e\u0440\u0438\u044f github.com\/siddhartha-gadgil\/ProvingGround.git<\/a>, \u0432 \u0441\u043b\u0443\u0447\u0430\u0435 \u043e\u0448\u0438\u0431\u043a\u0438 \u0437\u0430\u043f\u0443\u0441\u043a\u0430 Ammonite REPL \u0441\u043e\u0437\u0434\u0430\u0442\u044c \u043f\u0443\u0441\u0442\u0443\u044e \u0434\u0438\u0440\u0435\u043a\u0442\u043e\u0440\u0438\u044e ProvingGround\/mantle\/target\/web\/classes\/test<\/code>).\n<\/li>\n
  2. \u0412\u0442\u043e\u0440\u043e\u0439 \u2014 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043a\u043e\u043c\u0430\u043d\u0434\u044b sbt server\/run<\/code> \u0438 \u0437\u0430\u0442\u0435\u043c \u043e\u0442\u043a\u0440\u044b\u0442\u044c \u0432 \u0431\u0440\u0430\u0443\u0437\u0435\u0440\u0435 http:\/\/localhost:8080<\/a>.\n<\/li>\n
  3. \u0422\u0440\u0435\u0442\u0438\u0439 \u2014 \u0438\u0437 IDE. \u0412 IntelliJ Idea 2017.1.3 \u043f\u0440\u043e\u0435\u043a\u0442 \u043c\u043e\u0436\u0435\u0442 \u0438\u043c\u043f\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u0442\u044c\u0441\u044f \u043f\u043e\u0441\u043b\u0435 \u043c\u043e\u0434\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438<\/a> build.sbt, \u043d\u043e \u043a\u043e\u0434 \u043c\u043e\u0436\u0435\u0442 \u043d\u0435 \u0437\u0430\u043f\u0443\u0441\u043a\u0430\u0442\u044c\u0441\u044f. \u0420\u0435\u0448\u0435\u043d\u0438\u0435 \u2014 \u0438\u043c\u043f\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0432 \u0418\u0434\u0435\u044e \u043d\u0435 \u0432\u0435\u0441\u044c \u043f\u0440\u043e\u0435\u043a\u0442, \u0430 \u0442\u043e\u043b\u044c\u043a\u043e \u043f\u043e\u0434\u043f\u0440\u043e\u0435\u043a\u0442 ProvingGround\/core<\/code>. \u0414\u043b\u044f \u044d\u0442\u043e\u0433\u043e \u043d\u0443\u0436\u043d\u043e \u043f\u043e\u043b\u043e\u0436\u0438\u0442\u044c \u043d\u043e\u0432\u044b\u0439 build.sbt<\/a> \u0441\u044e\u0434\u0430: ProvingGround\/core\/build.sbt<\/code> .\n
      \u0421\u043f\u0438\u0441\u043e\u043a \u0438\u043c\u043f\u043e\u0440\u0442\u043e\u0432:<\/p>\n
    import provingground._ import HoTT._ import TLImplicits._ import shapeless._ \/\/import ammonite.ops._ import FansiShow._<\/code><\/pre>\n<\/li>\n<\/ol>\n
      \u0415\u0441\u043b\u0438 \u043a\u043e\u043c\u0443 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u0430 \u044d\u0442\u0430 \u0442\u0435\u043c\u0430 (\u0442\u0435\u043e\u0440\u0438\u044f \u0442\u0438\u043f\u043e\u0432, \u0433\u043e\u043c\u043e\u0442\u043e\u043f\u0438\u0447\u0435\u0441\u043a\u0430\u044f \u0442\u0435\u043e\u0440\u0438\u044f \u0442\u0438\u043f\u043e\u0432, \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0435 \u0442\u0438\u043f\u044b, \u0432\u044b\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u044f \u043d\u0430 \u0443\u0440\u043e\u0432\u043d\u0435 \u0442\u0438\u043f\u043e\u0432, \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u0442\u0435\u043e\u0440\u0435\u043c), \u0434\u043e\u0431\u0440\u043e \u043f\u043e\u0436\u0430\u043b\u043e\u0432\u0430\u0442\u044c \u043d\u0430 \u043c\u043e\u0439 \u043a\u0443\u0440\u0441<\/a>. \u041e\u043d \u0432\u0432\u043e\u0434\u043d\u044b\u0439. \u041f\u043e HoTT \u0441\u043a\u043e\u0440\u0435\u0435 \u0434\u0430\u0436\u0435 \u043d\u0435 \u0432\u0432\u0435\u0434\u0435\u043d\u0438\u0435, \u0430 \u0432\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0432\u043e \u0432\u0432\u0435\u0434\u0435\u043d\u0438\u0435, \u043d\u043e \u043f\u043e \u043e\u0441\u0442\u0430\u043b\u044c\u043d\u044b\u043c \u043d\u0430\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u044f\u043c, \u0434\u0443\u043c\u0430\u044e, \u0434\u043e\u0442\u044f\u0433\u0438\u0432\u0430\u0435\u0442 \u0434\u043e \u0443\u0440\u043e\u0432\u043d\u044f \u043f\u0440\u043e\u0441\u0442\u043e \u0432\u0432\u0435\u0434\u0435\u043d\u0438\u044f. \u0421\u043f\u0430\u0441\u0438\u0431\u043e \u0437\u0430 \u0432\u043d\u0438\u043c\u0430\u043d\u0438\u0435.
     \u0441\u0441\u044b\u043b\u043a\u0430 \u043d\u0430 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b \u0441\u0442\u0430\u0442\u044c\u0438      https:\/\/habrahabr.ru\/post\/329176\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"
    \u0412\u0441\u0435\u043c \u043f\u0440\u0438\u0432\u0435\u0442. \u0425\u043e\u0447\u0443 \u043f\u043e\u0434\u0435\u043b\u0438\u0442\u044c\u0441\u044f \u0441\u0432\u043e\u0438\u043c \u043e\u043f\u044b\u0442\u043e\u043c \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u044f \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 ProvingGround<\/a>, \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043d\u043e\u0439 \u043d\u0430 \u0421\u043a\u0430\u043b\u0435 \u0441 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c Shapeless<\/a>. \u0423 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 \u0438\u043c\u0435\u0435\u0442\u0441\u044f \u0434\u043e\u043a\u0443\u043c\u0435\u043d\u0442\u0430\u0446\u0438\u044f<\/a>, \u043f\u0440\u0430\u0432\u0434\u0430, \u043d\u0435 \u043e\u0447\u0435\u043d\u044c \u043e\u0431\u0448\u0438\u0440\u043d\u0430\u044f. \u0410\u0432\u0442\u043e\u0440 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 \u2014 \u0421\u0438\u0434\u0434\u0445\u0430\u0440\u0442\u0445\u0430 \u0413\u0430\u0434\u0436\u0438\u043b<\/a> \u0438\u0437 Indian Institute of Science. \u0411\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 \u044d\u043a\u0441\u043f\u0435\u0440\u0438\u043c\u0435\u043d\u0442\u0430\u043b\u044c\u043d\u0430\u044f. \u0421\u0430\u043c \u0421\u0438\u0434\u0434\u0445\u0430\u0440\u0442\u0445\u0430 \u0433\u043e\u0432\u043e\u0440\u0438\u0442, \u0447\u0442\u043e \u044d\u0442\u043e \u043f\u043e\u043a\u0430 \u043d\u0435 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430, \u0430 \u00abwork in progress\u00bb. \u0413\u043b\u043e\u0431\u0430\u043b\u044c\u043d\u0430\u044f \u0446\u0435\u043b\u044c \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 \u2014 \u0431\u0440\u0430\u0442\u044c \u0441\u0442\u0430\u0442\u044c\u044e \u0436\u0438\u0432\u043e\u0433\u043e \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0430, \u043f\u0430\u0440\u0441\u0438\u0442\u044c \u0442\u0435\u043a\u0441\u0442, \u043f\u0435\u0440\u0435\u0432\u043e\u0434\u0438\u0442\u044c \u0435\u0441\u0442\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u044b\u0439 \u044f\u0437\u044b\u043a \u0441 \u0444\u043e\u0440\u043c\u0443\u043b\u0430\u043c\u0438 \u0432 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043c\u043e\u0433 \u0431\u044b \u0447\u0435\u043a\u0430\u0442\u044c \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0442\u043e\u0440. \u041f\u043e\u043d\u044f\u0442\u043d\u043e, \u0447\u0442\u043e \u0434\u043e \u044d\u0442\u043e\u0433\u043e \u0435\u0449\u0435 \u043e\u0447\u0435\u043d\u044c \u0434\u0430\u043b\u0435\u043a\u043e. \u041f\u043e\u043a\u0430 \u0447\u0442\u043e \u0432 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435 \u043c\u043e\u0436\u043d\u043e \u0440\u0430\u0431\u043e\u0442\u0430\u0442\u044c \u0441 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u043c\u0438 \u0442\u0438\u043f\u0430\u043c\u0438 \u0438 \u043e\u0441\u043d\u043e\u0432\u0430\u043c\u0438 \u0433\u043e\u043c\u043e\u0442\u043e\u043f\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0442\u0435\u043e\u0440\u0438\u0438 \u0442\u0438\u043f\u043e\u0432 (HoTT<\/a>), (\u043f\u043e\u043b\u0443-) \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u0442\u0435\u043e\u0440\u0435\u043c\u044b.  <\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"class_list":["post-286672","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/286672","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=286672"}],"version-history":[{"count":0,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/286672\/revisions"}],"wp:attachment":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=286672"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=286672"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=286672"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}