## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

No credit card required

## Propositions Are Types, and Proofs Are Programs

We can use any values of arbitrary complexity inside type expressions, not just simple values like numbers. We can even encode logical propositions too, and use these to express pre and post conditions, and more. For example, the following represents a property of equality—that when two things are equal, then what we can do with one thing, we can do with the other.

 ​ foo2 :: (A:Type)(P:A -> Type)(a,b:A)Eq A a b -> P(a) -> P(b)

We can do more than just encode logical propositions: we can work with proofs of them entirely inside the language as well. If you’ve done any logic before, you may recognize the following as a statement of transitivity of implication. “If B implies C, and A implies B, then ...

## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

No credit card required