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.
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.