In Martin-Löf type theory, the notion of equality is basic, and for every type $A$ and elements $x, y \in A$ there is a type $x =_A y$. For any function $f\colon A \to B$ you can then prove $f(x) =_B f(y)$ from $x =_A y$. In some systems, such as homotopy type theory, you can also construct quotient types, making a new type $Q$ where you get to specify what $=$ is, which then must be respected by all functions out of $Q$.
However, apartness often has more constructive content than equality. Are there any type theories that take apartness to be basic, and allow quotients? That is, have an apartness $x \neq_A y$ for any $x, y \in A$, can prove that every function $f\colon A \to B$ is strongly extensional ($f(x) \neq_B f(y)$ implies $x \neq_A y$), and given an apartness relation $\#$ on a type $A$ can construct a quotient $Q$ where $\neq_Q$ corresponds to $\#$. It seems like having all functions out of the reals be strongly extensional would be useful for constructive real analysis. On the other hand, homotopy type theory shows that equality can also have constructive content, which makes me wonder if both equality and inequality could be made basic, rather than defining one as the negation of the other.