In general, there are credible early attempts to study aspects of mathematics in the context of paraconsistent calculi (there are many, just look at the ToC of Priest's textbook).
That said, the answer to the precise question you actually asked, the one regarding type theory, is negative.
In type theory (as in most foundational systems), the statement $0=1$ is naturally explosive, in the sense that you can prove anything using $0=1$ without ever invoking $\bot$-elimination. Why? As in my answer to your other question about type theory, given types $A,B$, you can use $\mathbb{N}$-induction to construct a function $f: \mathbb{N} \rightarrow \mathcal{U}$ such that $f(0)$ reduces to $A$ and $f(Sn)$ reduces to $B$. Applying the congruence rule to $0=1$ yields $A = B$, so all types are equal, and in particular $A \rightarrow B$ holds. In fact, Martin-Löf type theory is maximally explosive: if you can inhabit a type $T$ in the empty context without using $\bot$-elimination, an induction on the structure of the proof shows that you could have inhabited the type $T^{\bot \leftarrow 0=1}$, the type obtained from $T$ by replacing every occurrence of $\bot$ with $0=1$. There is nothing specific about $0=1$ here: Martin-Löf type theory without explosion is really just a world where $\bot$ denotes an arbitrary proposition. In particular, if $A$ does not mention $\bot$, then MLTT without explosion proves $A \rightarrow \bot$ precisely if $A$ is explosive.
This means that, as long as you don't intend to add new, classically inadmissible principles, there is not much point in studying these "minimal" type theories based on minimal logic. The situation is more interesting in e.g. the variant of Heyting arithmetic that uses minimal logic instead of intuitionistic logic as its logical substrate. This theory is almost, but not quite, the same as full intuitionistic Heyting arithmetic, since $0=1$ is explosive.
For example, if you want to prove using $0=1$ that every number is even, you can multiply the inconsistent equality by $2$ to get $0=2$, apply transitivity to get $1=2$, then replace $1$ with $2$ in $\forall x. 1x = x$ to conclude $\forall x. 2x=x$, and then $\forall x. \exists y. 2y=x$. You can do this systematically (by induction on the structure of the formula $A$) to prove that $0 = 1 \rightarrow A$.
This time, the converse does not hold, and Heyting arithmetic formulated in minimal logic is not maximally explosive: there are positive statements that it proves false, but that are not explosive. That's because one of the axioms of Heyting arithmetic says something non-trivial about $\bot$. There are two ways to conclude $\bot$ in Heyting arithmetic:
From an induction axiom. This is not a problem: when you replace all occurrences of $\bot$ with $0=1$ in an induction axiom, the result is another induction axiom. (This is the only case in MLTT, which is why it justifies explosion.)
By applying the non-logical axiom $\forall x. 0 = Sx \rightarrow \bot$ to some $St = 0$. The problem is that you cannot replace this axiom with $\forall x. 0 = Sx \rightarrow 0 = 1$: it takes some work to show that this really cannot be done: it turns out that $0 = 2$ does not provably imply $0=1$ if you formulate Heyting arithmetic inside minimal logic. For details you can consult Heerkens' MSc thesis.
This is, however, the only obstacle: you replace $\forall x. 0 = Sx \rightarrow \bot$ with $\forall x. 0 = Sx \rightarrow 0 = 1$, and you get a minimal arithmetic that coincides perfectly with intuitionistic Heyting arithmetic. One can argue that this modified axiom is philosophically justified purely on basis of what we want arithmetic to be.
Best Answer
In intuitionistic mathematics, what we have is $$\forall x,y\quad x\#{}y\to x<y \lor y<x$$ where $\#$ is the intuitionistic notion of apartness. Now, if we define equality in terms of apartness and negation $$x=y\equiv{\lnot{x\# y}}$$ we have $$\forall{x,y}\quad \lnot (\lnot (x\leq y) \land \lnot (y\leq x))$$ which is classically, but not intuitionistically, equivalent to $$\forall x,y\quad x\leq y \lor y\leq x$$
Naturally, intuitionistic real numbers, which are defined by computable Cauchy sequences, can still have decimal expansions and integer parts.