We all learned about induction for proving properties of natural numbers at school. But what about other data types such as lists - do they have induction principles? And what exactly are properties and can we use induction for different notions of properties. Finally, if we work in categories other than the category of Sets, do we still have induction principles?

In this talk I'll show that, indeed, we can have induction principles parameterised by the category we work in, the data type we are interested in and the notion of property under consideration. These results arise from a very beautiful picture of induction if one will willing to consider the topic within a fibrational setting.