In Coq, the type of truth values is called Prop. In other foundations, it might be encoded differently, including by encoding functions into truth-values as functions out of an arbitrary type.
Current theme: default
Less Wrong (text)
Less Wrong (link)
In Coq, the type of truth values is called Prop. In other foundations, it might be encoded differently, including by encoding functions into truth-values as functions out of an arbitrary type.