By this I mean to ask, is it a bad idea to have all type constructor term expressions abstracted with $\mu$ just in case they need to be recursive? For example,
$Bool : Type;$
$Bool = (\mu Bool' . (Unit \lor Unit));$
The value constructors would still just be $(inj_0 unit)$ and $(inj_1 unit)$ in a system with equirecursive types, right? It seems like it would just be $O(x + 1)$ for an $O(x)$ type checking algorithm using unification, or maybe not even that.
I understand why $Bool$ is not written this way by default, especially considering recursive types are usually added to a theory after-the-fact and therefore the value constructors would differ depending on the variant of the recursive type theory. It's much less intuitive to read $(\mu X . \tau)$ than just $\tau$ when programming or proving theorems but are there any reasons of real consequence for not doing this? I can't find any.
The reason I ask this question is because I am writing a program to translate a functional programming language into a core dependent type theory with equirecursive types.