What is a type in type theory? I tried to find a rigorous definition without luck. And that makes me wonder.. maybe there isn't any rigorous definition?
My aim is to see how homotopy type theory provides a foundation for mathematics. An attempt is given here. Despite the nice resources given there, however, I found that my problem was more basic than knowing what a homotopy type theory is. Rather, it's about type theory: I'm in search of a rigorous definition of type theory.
Now, since this question is close to the fundamentals.. I reckon that I might have to specify what I really need. First of, I know how the basics of type theory works. I know that a type is roughly a collection of things, called terms, whatever these means. I know there might be rules to tell if a given term is of a given type. I know there are types derived from predefined types.. etc. If you ask me to follow the rules and play the game, I think I won't have a problem. What bothers me is that I don't really know what a type is, whenever addressed.
So, really, what is a type? What is a term? What is a function? Are they fundamentally undefined?
My feeling is.. it's necessary to introduce the rules of the game we're playing if one has to more rigorously refine type. And to do that, deductive system and lambda calculus seem to be a must. To define a function, it seems that certain realistic or imaginary machine should be involded.. for example Turing machine. And are there other systems to be introduced, before defining rigorously what a type is? Also, a natural question then arises: can all these systems be rigorously defined?
I have to admit at the end that I might not fully understand what I'm asking. I know I'm in search of a full and rigorous definition of type.. but you might ask what I mean by "rigorous"? Well.. I don't know. How can I define "rigorous"? How can I define "define"? What is "what"? And what is "what is what"? ..? It might sound like I'm making fun of words, but I'm serious.
EDIT: Zhen Lin asked a great question in the comment, which helped me express my expectation through set theory.
@ZhenLin I'm much comfortable with set theory because I sort of know what are undefined. We start with a set of undefined symbols (characters) and make up strings. There are some symbols that are "special": " ", "(", ")", "$\exists$", "$\forall$, "$\wedge$, "$\to$... etc. There is a list of pre-defined rules, that tell us how to reduce one to another. There is a list of pre-defined axioms that tell us where we could start. There is a list of translation rules that translate what's in it to English. And then we obtain meanings from that..