C. B. Aberlé - Parametricity via Cohesion

entics:14710 - Electronic Notes in Theoretical Informatics and Computer Science, December 11, 2024, Volume 4 - Proceedings of MFPS XL - https://doi.org/10.46298/entics.14710
Parametricity via CohesionArticle

Authors: C. B. Aberlé

    Parametricity is a key metatheoretic property of type systems, which implies strong uniformity & modularity properties of the structure of types within systems possessing it. In recent years, various systems of dependent type theory have emerged with the aim of expressing such parametric reasoning in their internal logic, toward the end of solving various problems arising from the complexity of higher-dimensional coherence conditions in type theory. This paper presents a first step toward the unification, simplification, and extension of these various methods for internalizing parametricity. Specifically, I argue that there is an essentially modal aspect of parametricity, which is intimately connected with the category-theoretic concept of cohesion. On this basis, I describe a general categorical semantics for modal parametricity, develop a corresponding framework of axioms (with computational interpretations) in dependent type theory that can be used to internally represent and reason about such parametricity, and show this in practice by implementing these axioms in Agda and using them to verify parametricity theorems therein. I then demonstrate the utility of these axioms in managing the complexity of higher-dimensional coherence by deriving induction principles for higher inductive types, and in closing, I sketch the outlines of a more general synthetic theory of parametricity, with applications in domains ranging from homotopy type theory to the analysis of program modules.


    Volume: Volume 4 - Proceedings of MFPS XL
    Published on: December 11, 2024
    Accepted on: November 11, 2024
    Submitted on: November 11, 2024
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,Mathematics - Category Theory

    Consultation statistics

    This page has been seen 29 times.
    This article's PDF has been downloaded 10 times.