It’s a ‘hunch’ but I think many-sorted theories corresponds well to many-sorted logic which corresponds to type theory which corresponds to typed lambda calculus.
In typed lambda calculus, there are two primitives of functions and types.
Types do not reduce to one another. They can be translated but always at a loss.
An alternative is untyped lambda calculus which has only functions but lacks the ability to be rigorously proven in first order logic for you can have TRUE = FALSE as they are seen as choices a and b, not as fundamentals.