$A\rightarrow B$ and $\Pi x:A.b(x)\in B$

Question

I have a question about the following two formulas (where both $A,B:\textsf{Prop}$ and $x$ is not a free variable in $B$): $$A\rightarrow B\quad\quad\quad\Pi x:A.b(x)\in B$$ where $b(x)\in B$ is a membership type (equivalent to $\textsf{Id}(b(x),b(x),B)$ using the notation of identity type) indicating that $b(x)$ is an inhabitant of $B$. It appears to me that they are equivalent. From $\Pi x:A.b(x)\in B$, by the elimination rule of $\in$, it is easy to deduce $\Pi x:A.B$, which is in fact equivalent to $A\rightarrow B$. So we have the following: $$(\Pi x:A.b(x)\in B)\rightarrow(A\rightarrow B)$$ But what about the other direction? Thanks in advance!

Answer 1

Let me expand a bit on Dan Doel's point. In Martin-Löf type theory, to make a judgement that $\operatorname{Id}(b(x),b(x),B)$ is a type, you need to have already judged that $b(x)$ is of type $B$. In particular, for $$\prod_{x:A}\operatorname{Id}(b(x),b(x),B)$$ to be a type, you need to know that we can deduce $b(x):B$ from $x:A$. This means you must assume that $\lambda x.b(x)$ is a term of type $A\rightarrow B$ for your question to even make sense. If we do assume this – ie, if we assume that we have already judged $\lambda x.b(x):(A\rightarrow B)$ – then we can solve your problem, but it's perhaps a slightly unsatisfying solution:

In Martin-Löf type theory, we have the "reflexive" constructor for identity types, which I will denote $\operatorname{refl}$. The introduction rule for $\operatorname{refl}$ is that, if $C$ is a type and we have judged $c:C$, then we can judge $\operatorname{refl}_c:\operatorname{Id}(c,c,C)$. If you have this construction in your type theory, then $\prod_{x:A}\operatorname{Id}(b(x),b(x),B)$ in fact always holds, with a proof given by the term $\lambda x.\operatorname{refl}_{b(x)}$. Since we know $b(x):B$ for any $x:A$, it is clear that this will be well-typed. If you wish, we can then construct a proof of $$(A\rightarrow B)\rightarrow\prod_{x:A}\operatorname{Id}(b(x),b(x),B),$$ simply by considering the term $\lambda f.\lambda x.\operatorname{refl}_{b(x)}$. Conversely, we can construct a proof of $$\prod_{x:A}\operatorname{Id}(b(x),b(x),B)\rightarrow (A\rightarrow B)$$ by the term $\lambda g.\lambda x.b(x)$; since we already know $\lambda x.b(x):(A\rightarrow B)$, this will be well-typed.

If this is the answer you're looking for, great! However, there's not much "moral" content in it, as the terms we construct don't ever use their first arguments. This is why I'm not sure if we're understanding your question correctly.