CoqでもLeanでもPropを使うが、Prepの正体は何でもよくて、デカルト閉半環圏（の対象集合）であればよい。自然数上に定義された述語 p は
- p: Nat → Prop
だが、その実体が次のいずれでも、さらに他の何かでもいい。
$`\quad p:{\bf N} \to {\bf B} \text{ in }{\bf Set}`$
$`\quad p:{\bf N} \to |{\bf Set}| \text{ in }{\bf SET}`$
CoqでもLeanでもPropを使うが、Prepの正体は何でもよくて、デカルト閉半環圏（の対象集合）であればよい。自然数上に定義された述語 p は
だが、その実体が次のいずれでも、さらに他の何かでもいい。
$`\quad p:{\bf N} \to {\bf B} \text{ in }{\bf Set}`$
$`\quad p:{\bf N} \to |{\bf Set}| \text{ in }{\bf SET}`$