I have to state that I am not very proficient in either one or the other, but at first glance they both seem to tackle similar concepts.
Wikipedia's definition of type theory:
In mathematics, logic, and computer science, a type theory is any of a
class of formal systems, some of which can serve as alternatives to
set theory as a foundation for all mathematics. In type theory, every
"term" has a "type" and operations are restricted to terms of a
certain type.
Wikipedia's definition of group theory:
In mathematics and abstract algebra, group theory studies the
algebraic structures known as groups. The concept of a group is
central to abstract algebra: other well-known algebraic structures,
such as rings, fields, and vector spaces, can all be seen as groups
endowed with additional operations and axioms.
These definitions strike me as very similar, as from my limited understanding:
- Type theory seems to be about how sets have types and how types relate to each other using relational axioms and operations that allow type inference and relational deduction using maps and functors,
- And group theory seems to be about studying axioms and operations that are defined to be applied to certain elements of a type, such as vectors, matrices…etc and using deduction to determine the "set" (as I interpret it) in which the desired result lies.
Am I right to perceive them as similar in nature, or am I misunderstanding the premises of both?
Best Answer
In my opinion, type theory and group theory are much different.
Type theory is a theory about foundations of mathematics, like logic and set theory. It aims to generalize the concept of set, so that, for example, we can talk about something like the 'set' of all sets, which is actually not a set.
Group theory is a branch of algebra. It does not care about any foundations of mathematics, just taking them for granted. A group is a set with a binary operation satisfying some axioms, which is a set indeed.