型宇宙 - pogi-log

型宇宙

型宇宙(type universe)

型宇宙は、要素が型であるような型

言い換え: 宇宙の要素が型

イメージとして↓の感じ

[型1, 型2, 型3, ... ] : 宇宙

変数名: 型名という記法で考えると

code:memo

type : Universe

$ \rm Type = Type_{0} \in Type_1 \in Type_2 \in ...

こういうのは可述的、階層を持つ型

Martin-Löf型理論から出てきた言葉の様子

初出はMartin-Löf (1975) [Palmgren1988]

ラッセル流宇宙、タルスキ流宇宙の記述スタイルがある？

最近の型理論：宇宙と世界、そして銀河

最近の型理論：宇宙・世界・銀河もう少し

最近の型理論：型理論の構文論と意味論

[Palmgren1988]『On Universe in Type Theory』

[Luo2012] 『Notes on Universes in Type Theory』

確認用

Q. 型宇宙

関連

グロタンディーク宇宙

参考

最近の型理論：宇宙・世界・銀河もう少し

メモ

type universe in nLab

［0009］宇宙

Type Polymorphism, Classes and Instances | Lectures

調査用

Google.icon 型宇宙(日)

Google.icon 型宇宙型理論(日)

Google.icon Type universe(英)

Wikipedia.icon

型宇宙 - Wikipedia(日)

型宇宙(検索) - Wikipedia(日)

Wikipedia.icon

Type universe - Wikipedia(英)

Type universe(検索) - Wikipedia(英)