Prop型
table:_
sort Prop型 (Sort 0) Type (Sort 1) Type 1 (Sort 2) Type 2 (Sort 3) ... type(型) True Bool Nat -> Type Type -> Type 1 ...
term(項) trivial true fun n => Fin n fun (_ : Type) => Type ...
Sort 0に対応する型なので、一般的な値と同じ宇宙に属しているということ
式tが命題p: Propの証明であるとは、t : pを満たすということ
命題 p : Prop があるとき、p 自体を型として解釈することができる。
上記の表を確認する
さらに、型 p を p の証明の型と解釈する。
つまり、型 p と型 Proof p を同一視する。
pが命題で、pの証明がt : pを満たすような、tということ
言い換えると、命題pがあって、
それを証明したいときは、
pが正しく型付できるような式tを構築すれば良い
t : pとなるような、tが1つでも見つかれば、命題pは真と言える
命題pが偽の場合、pを型付できるような項tが存在しない
pに空の型を関連付けることになる