\emph{Induction-recursion} is a definitional principle in Martin-L{\"o}f Type Theory defining families $(\U , \T: \U\to D) : \Fam{D}$ where $D: \Setone$ is an arbitrary fixed (large) set (which in motivating examples is ...