Set theory cares about sets and relations. And then functions are relations betweens sets of inputs and outputs.
Type theory, on the other hand, seems to say that there are no formal ideas of relations. At least this is my impression so far (and reason for the question).
As an example the homotopy type theory book uses the word "relation" dozens of times, but it does not seem to be formally defined.
Some quotes from the homotopy type theory book:
Given types $A$ and $B$, we can construct the type $A → B$ of functions with domain $A$ and codomain $B$. We also sometimes refer to functions as maps. Unlike in set theory, functions are not defined as functional relations; rather they are a primitive concept in type theory.
...
We may regard $R$ as a “proof-relevant relation” between $A$ and $B$, with $R(a,\ b)$ the type of witnesses for relatedness of $a\ :\ A\ and\ b\ :\ B$.
...
Homotopy is an equivalence relation, and operations such as concatenation, inverses, etc., respect it.
...
If a sequence $(a_n)_{n∈N}$ is defined by giving $a_0$ and specifying $a_{n+1}$ in terms of an, then in fact the $0th$ term of the resulting sequence is the given one, and the given recurrence relation relating $a_{n+1}$ to an holds for the resulting sequence.
In all of these cases (there are many more in the book), the word relation isn't formally defined in the type theory. Am I missing something? I don't have a deep understanding of type theory yet so it's difficult to tell.
Does type theory have a formal concept for relation? If not, why not, and how would you define a relation properly anyways? It would be very helpful to know how to mentally translate the set theory "relation" ideas into a type theory sort of way.
I'm no expert, but a relation can be treated as a function that maps to propositions. The book is written under the propositions = types paradigm, so a binary relation over types $A$ and $B$ is any element of the type $A \times B \rightarrow \mathfrak{U}$ where $\mathfrak{U}$ is the universe.