Harald König ; Uwe Wolter - Van Kampen Colimits and Path Uniqueness

lmcs:4022 - Logical Methods in Computer Science, April 25, 2018, Volume 14, Issue 2 - https://doi.org/10.23638/LMCS-14(2:5)2018
Van Kampen Colimits and Path UniquenessArticle

Authors: Harald König ; Uwe Wolter

    Fibred semantics is the foundation of the model-instance pattern of software engineering. Software models can often be formalized as objects of presheaf topoi, i.e, categories of objects that can be represented as algebras as well as coalgebras, e.g., the category of directed graphs. Multimodeling requires to construct colimits of models, decomposition is given by pullback. Compositionality requires an exact interplay of these operations, i.e., diagrams must enjoy the Van Kampen property. However, checking the validity of the Van Kampen property algorithmically based on its definition is often impossible. In this paper we state a necessary and sufficient yet efficiently checkable condition for the Van Kampen property to hold in presheaf topoi. It is based on a uniqueness property of path-like structures within the defining congruence classes that make up the colimiting cocone of the models. We thus add to the statement "Being Van Kampen is a Universal Property" by Heindel and Soboci\'{n}ski the fact that the Van Kampen property reveals a presheaf-based structural uniqueness feature.


    Volume: Volume 14, Issue 2
    Published on: April 25, 2018
    Accepted on: March 22, 2018
    Submitted on: October 27, 2017
    Keywords: Mathematics - Category Theory,18A15, 18A25

    1 Document citing this article

    Consultation statistics

    This page has been seen 1193 times.
    This article's PDF has been downloaded 439 times.