ホモトピー型理論 - mrsekut-p

ホモトピー型理論

直観主義型理論とホモトピーの融合

依存型と関係がある？

Univalence公理

同一性は同値性と同値である

https://homotopytypetheory.org/book/

学ぶならこの本らしい

オンラインで入手可能らしい

各所のリンクに出てきたキーワード

Observational Type Theory

Higher Topos Theory

様相ホモトピー型理論

https://golem.ph.utexas.edu/category/2020/02/modal_homotopy_type_theory_the.html

Introduction to Homotopy Type Theory

https://arxiv.org/abs/2212.11082

HoTTの入門的な教科書

Martin-Löfの依存型理論などの紹介

200以上の演習

型理論やホモトピー理論に関する知識は一切想定しない

ほんまか？mrsekut.icon

参考

https://uemurax.github.io/hott-ja/index.html

web上で日本語で読める資料

The HoTT Bookの読み方

https://m-a-o.hatenablog.com/entry/20130629/p1

https://www.ms.u-tokyo.ac.jp/publication/documents/2008tsuchiya.pdf

https://www.amazon.co.jp/Modal-Homotopy-Type-Theory-Philosophy/dp/0198853408/ref=sr_1_5?__mk_ja_JP=カタカナ&dchild=1&keywords=type+theory&qid=1588302586&sr=8-5

https://m-a-o.hatenablog.com/archive/category/HoTT

http://www.kurims.kyoto-u.ac.jp/~uemura/files/hott-intro-ja.pdf

http://phsc.jp/dat/rsm/2013_a3-1.pdf

https://www.slideshare.net/ssuser0745d1/ho-tt-introjp20160909

https://gist.github.com/yamarten/a60e9e4e1893c881cfb0e874a5d05b37

https://mathsoc.jp/publication/tushin/2004/2004shimakawa.pdf

https://m-a-o.hatenablog.com/entry/20120301/p1

https://github.com/mikeshulman/HoTT/tree/modalities

https://homotopytypetheory.org/2014/02/22/surreals-plump-ordinals/

『Homotopy Type Theory 入門』

https://uemurax.github.io/pdfs/hott-intro-ja.pdf