Difference Between A->B & A⊃B in Type Theory

[mXSCNT]

In type theory, what is the difference between the set of functions $$A \rightarrow B$$ and the implication set $$A \supset B$$? Is there any difference? My text says that both of them are examples of sets (propositions) that are defined as special cases of the cartesian product $$\prod(A,B)$$ (this cartesian product is the set of functions $$f(x)$$ from the index set $$A$$ to $$B(x)$$ where the image of $$x$$ lies in a set $$B(x)$$ that is itself dependent on $$x$$).

 

[Valkarie]

The main difference between the set of functions A \rightarrow B and the implication set A \supset B is that the former is a mapping from A to B while the latter is a statement that implies that all elements of A are contained in B. The set of functions A \rightarrow B is an example of a function, which is defined as a mapping from one set to another, while the implication set A \supset B is a statement that implies that all elements of A are contained in B. In terms of the cartesian product, the set of functions A \rightarrow B is defined as a subset of \prod(A,B) and the implication set A \supset B is not defined as a subset of \prod(A,B). Therefore, there is a difference between the two sets.