Now clearly \(B_{x,y}\) is nonempty if and only if \(R(x,y)\) holds. (We could have chosen any other element from our set theoretic universe than 0 to indicate truth.) Thus from any relation we can construct a family whose truth of \(x,y\) is equivalent to \(B_{x,y}\) being non-empty. Note that this interpretation does not care what the proof for \(R(x,y)\) is, just that it holds. Recall that intuitionistic type theory interprets propositions as types, so  \(p{:} {\rm Loves}({\rm John}, {\rm Mary})\) means that \({\rm Loves}({\rm John}, {\rm Mary})\) is true.