The function type A -> B corresponds to A => B in logic. This is a subtle but important difference between logic and type theory. In logic a statement is true o

The function type A -> B corresponds to A => B in logic. This is a subtle but important difference between logic and type theory. In logic a statement is true or false, but that's it. In type theory a statement (= type) has evidence (= values of that type). The type A -> B can be interpreted as turning evidence for A into evidence for B. The logical statements "for all x:A it's the case that B(x) holds" and "there exists a x:A such that B(x) holds" correspond to dependent function types `(x:A) -> B x` and dependent pair types `(x:A, B x)`, respectively. In intuitive terms "if you give me an x:A, then I give you evidence of B(x)", and "I give you an x:A, along with evidence of B(x)".