En théorie des catégories, une fibration représente une forme d'indexation d'une catégorie par une autre. On rappellera comment une telle structure peut être utilisée pour modéliser une logique (représentée par la catégorie indexée) au dessus d'une théorie des types (représentée par la catégorie index). On portera alors notre attention sur les types inductifs et coinductifs et comment capturer leurs schémas d'induction et de coinduction respectif dans les fibrations.