unit type
#Fleeting_Notes
unit type(単位型、ユニット型)
依存型理論の型の一つ
要素を一つ持つ
要素は$ \star
$ \mathbf{1} が型
$ \mathbf{1} の型は型宇宙$ \mathcal{U}
$ \mathbf{1} : \mathcal{U}
$ \star : \mathbf{1}
いろいろなプログラミング言語にunit typeに相当するものがある
Haskell, Rust, Elmの()
JavaScript
Null, Undefined
C/C++のvoid型
void型は空型ではない
厳密にはunit typeとして整合しない部分がある？
NULLという値の型は、型理論として考えるとunit type
対応するもの
(論理) true
(集合) シングルトン
(圏論) 終対象
(圏論) n-truncation: (-2)-truncated object
(型理論) unit type
(型理論) h-level 0型(h-level 0 type)
HoTTでの対応
(homotopy level) h-level 0
(n-truncation) (-2)-truncated object
(ホモトピー論) contractible space
(高次圏論) (-2)-groupoid
(高次トポス) -
(ホモトピー型理論) true
(ホモトピー型理論) unit type
(ホモトピー型理論) 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
computational trilogy in nLab
メモ
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(英)