Mathematics is often said to be about counting, about numbers. Yet currently, a very active group of mathematicians are proposing that arrows (category theory) are the natural language of mathematics. I will attempt to give some insights into this field of research called type theory, located at the intersection of foundations of mathematics, theoretical computer sciences and analytic philosophy. The level and language of the presentation will be adjusted to the interests and needs of those attending it.