Coqの宇宙は {Set, Prop} → Type → Type → ...
Leanの宇宙は Prop → Type → Type → ...
Typeには番号が付く。別にどっちでもいい。圏論的には次の圏を準備する。$`\newcommand{\mrm}[1]{\mathrm{#1}}
`$
- $`{\bf Ded}`$
- $`{\bf Set}`$
- $`{\bf SET}`$
- $`{\bf CAT}`$
次のように呼ぶ。
- $`\mrm{Prop} := \mrm{Obj}({\bf Ded})`$
- $`\mrm{Proof} := \mrm{Mor}({\bf Ded})`$
- $`\mrm{Type} := \mrm{Obj}({\bf Set})`$
- $`\mrm{Kind} := \mrm{Obj}({\bf SET})`$
次が成立する。
- $`\mrm{Type} \in \mrm{Kind}`$
- $`\mrm{Prop} \in \mrm{Kind}`$
