unit type
#Fleeting_Notes
unit type(単位型、ユニット型)
依存型理論の型の一つ
要素を一つ持つ
要素は$ \star
$ \mathbf{1} が型
$ \mathbf{1} の型は型宇宙$ \mathcal{U}
$ \mathbf{1} : \mathcal{U}
$ \star : \mathbf{1}
いろいろなプログラミング言語にunit typeに相当するものがある
void
()
JavaScript
Null, Undefined
NULLという値の型は、型理論として考えるとunit type
対応するもの
(論理) true
(集合) シングルトン
(圏論) 終対象
(圏論) n-truncation: (-2)-truncated object
(型理論) unit type
(ホモトピー型理論) h-level 0型/contractible type
確認用
Q. unit type
参考
unit type in nLab
『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 2 Homotopy type theory P86
Unit type - Wikipedia
メモ
void
None
singleton type
Unit type - Wikipedia
レコード型 -- ホモトピー型理論
調査用
Google.icon 単位型(日)
Google.icon Unit type(英)
Wikipedia.icon
単位型 - Wikipedia(日)
単位型(検索) - Wikipedia(日)
Wikipedia.icon
Unit type - Wikipedia(英)
Unit type(検索) - Wikipedia(英)