Unfortunately copy/paste doesn't work for this paper Inductive Definitions and Type Theory, but here is a snippet.
The paper begins by stating:
The first sentence of the second paragraph says type theory as a theory of inductive definitions. I have never really paid much attention to how central induction is to type theory, but it seems to be one of the main requirements, hence this question.
Is induction a requirement for type theory? That is, can you have a modern robust type theory or typed programming language without induction? If not, why not? If so, what would it look like generally speaking (just looking for pointers for the right research to look into). Why is induction central to type theory? What does type theory as a theory of inductive definitions mean?
Sorry if this is a really basic question. I am just trying to get a solid grasp of the foundations, and asking anything that is unclear to me in the process without having a full picture and being an expert yet.