Definitional Functoriality for Dependent (Sub)Types

Authors:
Preprint
Publisher website
Google Scholar
  • 23 October 2023
    • preprint
    • Published by HAL in HAL
Abstract
Dependently-typed proof assistant rely crucially on definitional equality,which relates types and terms that are automatically identified inthe underlying type theory.This paper extends type theory with definitional functor laws,equations satisfied propositionally by a large class of container-like typeconstructors F : Type → Type, equipped with a mapF : (A → B) → F A → F B$, such as lists or trees.Promoting these equations to definitional ones strengthen the theory, enablingslicker proofs and more automation for functorial type constructors.This extension is used to modularly justify a structural form of coercivesubtyping, propagating subtyping through type formers in a map-like fashion.We show that the resulting notion of coercive subtyping, thanks to the extradefinitional equations, is equivalent to a natural and implicit form ofsubsumptive subtyping.The key result of decidability of type-checking in a dependent type systemwith functor laws for lists has been entirely mechanized in Coq.

This publication has 27 references indexed in Scilit: