## 1 Introduction  
During recent decades, systems have become more complex as they evolved towards having multiple features and due to the rise of mechatronic design. This complexity leads to a need to create numerous models in system design. We use these models to represent the product towards diverse modeling intents, thus allowing the analysis of specific properties. Among these models, we find system engineering models used to apprehend complexity in the system. System engineering encompasses many models, including requirement and architecture models, safety models, and multi-physics models. These models are written by different people, using various tools and formalisms. This independence can lead to problems with consistency between the models. As diverse models represent one system, we fear that some models may contain errors, making them incompatible with the designed system. Such inconsistencies can be very concerning in the case of safety-critical systems and their safety models, and manual review of the models is time expensive. This is especially true of complex systems that can interact with humans, such as autonomous vehicles or cobots. Autonomous systems are complex and critical systems with highly complex control loops [1] that require advanced models when engineers simulate them. An undetected error in the safety model could lead to not considering some of the system's potential failure events. Such errors would then result in the system being dangerous for the user. When systems have to be certified in order to be accepted into the market, e.g., for planes, the safety assessment methodology needs to be accepted by safety authorities. This requires great trust in the safety assessment process and, therefore, in the consistency of the models. The system engineering community proposes different methodologies such as model federation [2] or proof theory approach [3] to assert and maintain consistency between these models to face this challenge. Amongst them, we find synchronization methodologies [4]. In this work, we address the mathematical aspect of the synchronization methodologies. The synchronization methodologies consist of three steps: first, we translate the models to a common formalism; then, we compare them in this common formalism; and finally, we carry the comparison results back to the original models. Although those methodologies exist and provide means to minimize the number of contradictions between the models, there is no formal definition of what consistency the community would widely accept. We primarily understand consistency by the absence of contradiction between the models, but this is not a criterion that single-handedly allows a methodology's efficiency to be demonstrated. Thus, we propose a formal definition of a binary consistency relation. In this work, we propose to use category theory to interpret the model synchronization through a mathematical framework. We aim to provide a tool that helps design and validate model synchronization methodologies mathematically. To achieve this goal, we give a mathematical representation of the comparison models that the synchronization methodologies use, and we propose a definition of a general consistency relation between models. We apply this mathematical framework to the SmartSync methodology [5] through the study of model consistency in the design workflow of an autonomous critical system, a fixed-wing blood delivery drone. In the SmartSync methodology, the comparison models are mathematically depicted through quintuples that contain their characteristics. The mathematical framework described in this work proposes an equivalent definition of the comparison models, representing the models through categories rather than quintuples. This new definition allows our mathematical framework to give a new mathematical perspective of the comparison, which allows for mathematical proofs of the properties compared between the models.