Mapping

A mapping $\bar{f}:A\to B\to \mathrm{Prop}$ is a kind of binary relation in which the following two properties hold:

• Left-Total: $\forall a:A.\exists b:B.\bar{f}ab$.
• Right Unique: $\forall b:B.\forall a_1,a_2:A.\bar{f}{a}_{1}b\wedge \bar{f}{a}_{2}b⟹a_1=a_2$.

The mapping itself is often written simply as:

$$f:A\to B$$

Equivalence in Type Theory

In type theory, it is required that $B$ is a set to ensure $fx=y$ are propositions. Additionally function extensionality and proposition extensionality are required.