Does type-theory have a concept of "relation"? 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.
 A: 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.
A: Here is a (naive) way to think about relations in type theory, as opposed to set theory.
Let us focus on binary homogeneous relations (i.e. relations that have two arguments of the same "nature").
In set theory, a homogeneous binary relation on a set $X$ is a subset $\mathcal{R} \subset X \times X$.

In type theory, a homogeneous binary relation between terms of
type $T$ is a term $R$ of type $$T \to (T \to \mathrm{Prop})$$
i.e. a function sending a term of type $T$ to a function from
terms of type $T$ to terms of type $\mathrm{Prop}$.

By (un)currying, such an $R$ can also be seen as a term of type $T\times T \to \mathrm{Prop}$, i.e. a function sending a term of type $T\times T$ to a term of type $\mathrm{Prop}$.
Intuitively, the type $\mathrm{Prop}$ consists of terms that are correct mathematical statements, in the sense that they have proofs. More formally, the terms of type $\mathrm{Prop}$ are themselves types, whose terms are thought of as proofs of the corresponding mathematical statements. So, here, if $t_1,t_2$ are terms of type $T$, the term $R(t_1,t_2)$ is a (true) mathematical statement. In view of the preceeding remark on currying, the term $R(t_1, t_2)$ can also be written $R\ t_1\ t_2$, but I will refrain from using this notation here.

The point is: if $a$ and $b$ are terms of type $T$, then $R(a,b)$
is a term of type $\mathrm{Prop}$.

In set theory, the pair $(a,b)$ is an element of the set $X\times X$, which may or may not belong to the subset $\mathcal{R} \subset X\times X$.
One can define similarly $n$-ary relations (not necessarily homogeneous) between terms of types $T_1, \ldots , T_n$ as terms of type $(T_1 \times \ldots \times T_n) \to \mathrm{Prop}$ (or, in set theory, as subsets of a product set $X_1\times\ldots\times X_n$).
It seems interesting here, as a first example of how to manipulate the concept of relation, to see what the definition of an equivalence relation looks like from the point of view of type theory.
By definition, an equivalence relation is a (homogeneous binary) relation that is reflexive, symmetric and transitive:

*

*Reflexivity: $\forall\ (t : T),\ R(t,t)$. This means that, for all term $t$ of type $T$, the proposition $R(t,t)$ has a proof. In other words, $R(t,t)$ is a true statement.

*Symmetry: $\forall\ (t_1\ t_2 : T),\ R(t_1,t_2) \to R(t_2,t_1)$. The notation $R(t_1,t_2) \to R(t_2,t_1)$ refers to a function between the types $R(t_1,t_2)$ and $R(t_2,t_1)$. Having a function $f : T_1 \to T_2$ between two types means that if we are given a term $t_1 : T_1$ (= a term $t_1$ of type $T_1$), it has an associated term $f(t_1) : T_2$ (i.e. $f(t_1)$ is a term of type $T_2$). Here it means that, if $R(t_1,t_2)$ is true, then $R(t_2,t_1)$ is true, which formalises the symmetry of the relation $R$.

*Transitivity is a bit more notationally involved: $$\forall\ (t_1\ t_2\ t_3 : T),\ R(t_1,t_2)\ \to \big(\ R(t_2,t_3) \to R(t_1,t_3)\ \big),$$ which means that, given a proof of $R(t_1, t_2)$, a proof of $R(t_2,t_3)$ gives a proof of $R(t_1,t_3)$. Equivalently, to a pair $(a,b)$ consisting of a proof $a$ of $R(t_1,t_2)$ and a proof $b$ of $R(t_2,t_3)$, there is associated a proof of $R(t_1,t_3)$, that we can denote by $f(a,b)$, where $f$ is the function $R(t_1,t_2)\times R(t_2,t_3) \to R(t_1,t_3)$ defined by $(t_1, t_2,t_3)$ in view of the transitivity axiom above.

One possible reference for this is the book Theorem proving in Lean, by Jeremy Avigad, Leonardo de Moura and Soonho Kong (see more specifically here for the definition of an equivalence relation, and here for more details on the type $\mathrm{Prop}$).
For the sake of completeness, let us compare with the set-theoretic definition of an equivalence relation $\mathcal{R} \subset X \times X$:

*

*Reflexivity: $\forall\ x\in X$, $(x,x)\in\mathcal{R}$.

*Symmetry: $\forall\ (x,y)\in X\times X$, $(x,y)\in\mathcal{R} \Rightarrow (y,x)\in\mathcal{R}$.

*Transitivity: $$\forall\ (x,y,z)\in X\times X \times X,\ \big(\ (x,y)\in \mathcal{R}\ \wedge\ (y,z)\in \mathcal{R}\ \big)\ \Rightarrow\ (x,z)\in\mathcal{R}.$$
Both approaches are seen to formalise the same concept.
