Definitional Functoriality for Dependent (Sub)Types - Extended Version

This paper extends Martin-Löf Type Theory (MLTT) with definitional functor laws for type constructors like lists, trees, and dependent products, enabling slicker proofs and more automation for functorial type constructors. It also uses this functorial structure to modularly justify a structural form of coercive subtyping.