HoTT(ホモトピー型理論) はホモトピー論や∞圏論を型システムの上で展開しようという考え方である。この体系は既にCoqで形式化が進んでいる。これはその使い方の覚書である。
まず、HoTT/Coqではなく、HoTT全般に関係する資料について述べる。
- HoTTの本家サイト http://homotopytypetheory.org/ に情報がたくさんある。この分野は数学の他分野に比べて、インターネット上に情報がより集約されているという特徴がある。
- HoTTについて紙面で勉強するならば、上のサイトにあるHoTT Bookを読むのが最も適切である。
