型
#Fleeting_Notes
型(type)
型は
ホモトピー型理論
の立場では
∞-グルーポイド
の構造になっている
別の言い方で
型は高階の亜群(グルーポイド)である
データを区別するために利用される
何をどんな風に区別できるかは
型システム
という体系(system)によって異なる
対応するもの
(論理)
命題
(集合)
集合
(圏論)
対象
(圏論)
0-truncated object
(型理論)
型
(ホモトピー論) 空間
(ホモトピー型理論)
h-set
確認用
Q. 型
関連
型をホモトピー的に扱う
Homotopy Type Theory(HoTT)
ソート
Sort 1
(Lean)
データ型
メモ
homotopy type theory in nLab
『灼熱のホモトピー型理論入門』
.
https://event.phys.s.u-tokyo.ac.jp/physlab2024/pdfs/article/spm_kouen.pdf
型は高階の亜群(グルーポイド)である
調査用
Google.icon
型(日)
Google.icon
Type(英)
Wikipedia.icon
型 - Wikipedia(日)
型(検索) - Wikipedia(日)
Wikipedia.icon
Type - Wikipedia(英)
Type(検索) - Wikipedia(英)