Is category theory just type theory with different words? According this this category theory provides a semantics for type theory. To me this means that category theory and type theory are essentially the same system just with different words.
In fact this seems to mean there is an isomorphism between type theories and category theories.
Just change the word 'type' to 'category'.
Thus if type theory and category theory have converged on the same mathematical and grammatical structure, what is the point of keeping the two systems. Shouldn't the mathematical community just get rid of either type theory or category theory and just keep one of them?
 A: First a technical point. You would have to define what an isomorphism between type theory and category theory is supposed to be using a meta theory if you would like to claim that such an isomorphism exists.
Second, you are partially right. The trinity between type theory, category theory and logic suggest that they are all inter-related. You can express any of those topics in term of the other.
The reason why you do not discard any of them is because they provide different viewpoints towards the same concept.
To give you an analogy, this is similar to the basic advantage of proof theory where you consider proof as mathematical objects, in the end if you have a proof of the fundamental theorem of calculus and a proof that two triangles are similar, they both encode the information "true" but in a very different way. You will not supposedly, discard one for the other.
Now the different viewpoints are :

*

*Logic -> Proof theory. There is an emphasis in manipulating proof as mathematical objects in your deductive system.


*Type theory -> algorithms. There is an emphasis in manipulating algorithms which are just a collection of instructions.


*Category Theory -> algebra. Here the emphasis is on manipulating algebraic objects using algebraic rules.
It is best to get comfortable with these different viewpoint as any can provide you meaningful information about the other as the past has shown consistently.
Hope that helps !
