levelsio

<?
/////////////////////
// slack2html
// by @levelsio
/////////////////////
//
/////////////////////
// WHAT DOES THIS DO?
/////////////////////
//

qnighy

はじめに

HoTT(ホモトピー型理論) はホモトピー論や∞圏論を型システムの上で展開しようという考え方である。この体系は既にCoqで形式化が進んでいる。これはその使い方の覚書である。

HoTTの参考資料

まず、HoTT/Coqではなく、HoTT全般に関係する資料について述べる。

• HoTTの本家サイト http://homotopytypetheory.org/ に情報がたくさんある。この分野は数学の他分野に比べて、インターネット上に情報がより集約されているという特徴がある。
• HoTTについて紙面で勉強するならば、上のサイトにあるHoTT Bookを読むのが最も適切である。

belbomemo

         ,_---~~~~~----._         
  _,,_,*^____      _____``*g*\"*, 
 / __/ /'     ^.  /      \ ^@q   f 
[  @f | @))    |  | @))   l  0 _/  
 \`/   \~____ / __ \_____/    \   
  |           _l__l_           I   
  }          [______]           I  
  ]            | | |            |  
  ]             ~ ~             |  
  |                            |