Group theory vs Type theory 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?
 A: 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. 
A: One way to see that group theory and type theory are orthogonal, is the fact that you can define a group in a type theory. Using a standard type theory with $\Pi$ and $\Sigma$ types, we can define a group as anything with the following type:
\begin{align}
  \newcommand\op{\!\cdot\!}
  \sum_{G : \mathfrak{U}}
  \sum_{{}\cdot{}: G \to G \to G}
  \sum_{e:G}
  \left(
    \prod_{a,b,c:G}\! (a \op b) \op c = a \op (b \op c)
    \lower{0.5em},
    \prod_{a:G} (a \op e = a,\, e \op a = a)
    \lower{0.5em},
    \prod_{a:G} \sum_{b:G} (a \op b = e,\, b \op a = e)
  \right)
\end{align}
Here $G$ is the set, $\cdot$ is the group operation, and $e$ is the identity element, and then the triple of $\Pi$-types represents the three laws that the group operation must obey. (We only have three since the type of the group operation, $\cdot : G \to G \to G$ gives us closure for free.) 
A: I also think they are used very differently by mathematicians. 
First note that while there is "group theory", the theory of groups, we should speak of a type theory. There is no "type theory" which would be "the theory of types". There are lots of type theories, depending on what kind of constructions you allow within your theory.
Also, a type theory is a purely formal system : just like set theory doesn't bother defining what a set is, there is no definition of what a type is in type theory (this being said, there are of course interpretations of type theory in other more "conventional" theories, like homotopy type theories, which in a sense aim to give a construction of what a type is).
On the other hand, a group, is a "concrete" object : we know what a group is, it's not purely formal. This being said, I guess you could see a group as a formal system with rewriting rules (I don't really know what that would look like or what use it would have, but I don't think it's an absurd notion) ; this is just not the point of view of mathematicians.
