When we talk about dependent types, we often take an informal approach, trying to initiate people with more or less simple examples. Unfortunately, with such an approach, we fail to understand the very essence of type dependency, which goes right over our heads.In this presentation, we're going to step out of our comfort zone right from the start, starting with theory and moving on to practice. Starting with theory means reading formalisms to better understand what type dependency is all about! To do this, we'll be looking at the dependent functional type and the dependent pair.