The Intermediate value theorem comes to mind.
If $f$ is continuous on a closed interval $[a,b]$, and $c$ is any number between $f(a)$ and $f(b)$ inclusive, then there is at least one number $x$ in the closed interval such that $f(x)=c$.
While it looks very theoretically in nature, it is the foundation for a lot of real analysis. It is important for numerical proofs, and in turn numerical mathematics is important for e.g. Computer Tomography.
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
There are four definitions which are classically equivalent to being finite. Let $[n]$ be the set $\{0, 1, ..., n - 1\} = \{m \in \mathbb{N} \mid m < n\}$.
Note that all these definitions are bijection-invariant. That is, if $A \cong B$ (that is, if there is a bijection $A \to B$), then $A$ satisfies definition $i$ if and only if $B$ does.
You may have noticed that definitions 4 and 5 are similarly named. This is because
Proof: Suppose that $S$ is sub-finitely enumerable (definition 4). Without loss of generality, suppose $S \subseteq K$ where $K$ is finitely enumerable. Take a surjection $f : [n] \to K$. Consider $S' = f^{-1}(S) \subseteq [n]$, which is clearly subfinite. Then $f|_{S'} : S' \to S$ is surjective. Therefore, $S$ is subfinitely enumerable (definition 5).
Now suppose that $S$ is subfinitely enumerable (definition 5). Without loss of generality, let $K \subseteq [n]$ and $f : K \to S$ be a surjection. Define $\sim \subseteq [n]^2$ by $a \sim b$ if and only if either $a = b$ or $a, b \in K$ and $f(a) = f(b)$. Consider the quotient set and map $\pi : [n] \to [n] / \sim$. Note that $\pi$ is surjective, demonstrating that $[n] / \sim$ is finitely enumerable.
Define $g : S \to [n] / \sim$ by $g(f(x)) = \pi(x)$. Note that $g$ is well-defined, since if $f(x) = f(y)$ then $x \sim y$ and thus $\pi(x) = \pi(y)$, so $g(f(x)) = \pi(x) = \pi(y) = g(f(y))$. And note that since $f$ is surjective, it's defined on all of $S$.
I claim that $g$ is an injection. For suppose that $g(a) = g(b)$. Write $a = f(x)$, $b = f(y)$. Then $\pi(x) = \pi(y)$. Then $x \sim y$. Then $f(x) = f(y)$. Then $a = b$.
Therefore, $S$ is sub-finitely enumerable (definition 4). $\square$
From here on out, we use sub-finitely enumerable and subfinitely enumerable interchangably.
We see that subfinitely enumerable is the definition you're looking for.
If $S$ is subfinitely enumerable, then we have an injection $f : S \to K$ where $K$ is finitely enumerable. If we have $S' \subseteq S$, then we have $f|_{S'} : S' \to K$ is also an injection, as the composition of the inclusion injection $S' \subseteq S$ and the injection $f : S \to K$. So $S'$ is subfinitely enumerable. So subfinite enumerability is closed under the taking of subsets.
If $S$ is subfinitely enumerable, then we have a surjection $f : K \to S$ where $K$ is subfinite. Suppose we have some equivalence relation $\sim$ on $S$. Then $\pi : S \to S / \sim$ is a surjection, so $\pi \circ f : K \to S / \sim$ is a surjection as the composition of surjections. Therefore, $S / \sim$ is subfinitely enumerable.
Note that "subfinitely enumerable" is therefore the smallest class $\mathbf{C}$ of sets such that (1) if $A \approx B$ and $A \in \mathbf{C}$, then $B \in \mathbf{C}$ (2) if $S \in \mathbf{C}$ and $S' \subseteq S$ then $S' \in \mathbf{C}$, (3) if $S \in \mathbf{C}$ and $\sim$ is an equivalence relation on $S$, then $S / \sim \in \mathbf{C}$, and (4) for all $n \in \mathbb{N}$, $n \in \mathbf{C}$.
Assuming the existence of power sets and of $\mathbb{N}$, the full subcategory of subfinitely enumerable sets and functions between them is essentially small. This is because every subfinitely enumerable set can be placed into a bijection with some subset of $[n] / \sim$ for some equivalence relation $\sim$ on $[n]$. So a subfinitely enumerable set is exactly a set which can be placed into bijection with some element of $\{S \mid S \subseteq [n] / \sim, n \in \mathbb{N}, \sim$ is an equivalence relation on $[n]\}$.
One final note: if you're familiar with topos theory, the proof that definitions (4) and (5) coincide can be made quite simple. For (4) implies (5), we can simply take the pullback of $[n] \to K \leftarrow S$ and use the fact that the pullback of a mono is a mono, and the pullback of an epi is an epi (in a topos). For (5) implies (4), we can take the pushout of $[n] \leftarrow k \to S$ and use the fact that the pushout of a mono is mono (in a topos), and the pushout of an epi is an epi.