Towards Directed Model Categories

多年来，数学家们一直在研究拓扑学，拓扑学指的是在连续变形下不变的形状和空间。直观地说，这相当于将形状视为可拉伸和可收缩的，但不撕裂它们。拓扑学应该捕捉几何“，就好像一切都是由橡胶制成的。“不过，这还不够强。由于各种原因，我们常常想把拓扑学上升到同伦。这意味着像马克杯和甜甜圈这样的形状应该被视为相同的形状。同伦理论在过去的世纪里有了惊人的发展，在过去的15年里，研究者们发现了同伦理论与形式逻辑之间的联系。有些令人惊讶的是，他们已经能够利用这些连接来丰富用于验证关键任务计算机系统（例如医疗设备，电网）的正确性和可靠性的各种软件。在一个不相关的工作流中，研究人员还开发了一种定向拓扑结构。这意味着我们仍然在研究几何形状，但我们只能在特定的方向上“行走”。例如，想象一个只能顺时针移动的圆。有向同伦理论在验证并发系统（即同时发生多个事件的软件）的良好行为方面有着显著的应用。然而，有向拓扑没有自己的“有向同伦理论”。“这样的理论将使与逻辑的联系成为可能，而逻辑又可以用来理解和研究不可逆变换的行为，包括并发计算机系统的功能。该项目旨在为发展这种理论奠定基石。它将通过尝试使“模型范畴”的基本技术概念适应于有向拓扑来做到这一点。

For many years mathematicians have studied topology, which refers to shapes and spaces that are invariant under continuous deformation. Intuitively, this amounts to treating shapes as strechable and contractible, but without tearing them.Topology is supposed to capture geometry "as if everything is made from rubber." However, even that is not strong enough. For various reasons we often want to think of topology up to homotopy. This means that shapes like a mug and a doughnut should be treated as the same. Homotopy theory has seen incredible development over the past century.In the last 15 years researchers have discovered connections between homotopy theory and the field of formal logic. Somewhat surprisingly, they have been able to take advantage of these connections to enrich various pieces of software that is used to verify the correctness and reliability of mission-critical computer systems (e.g. medical equipment, power grids).In an unrelated stream of work, researchers have also developed a version of topology that is directed. This means that we still study geometrical shapes, but we can only "walk" on them in a particular direction. For example, imagine a circle on which one can only move clockwise. This theory has found remarkable applications in verifying the good behaviour of concurrent systems, i.e. software in which more than one thing is happening at once.However, directed topology does not have its own "directed homotopy theory." Such a theory would enable connections with logic, which can in turn be used to understand and study the behaviour of non-reversible transformations, including the function of concurrent computer systems. This project aims to lay the foundational stone in developing such a theory. It will do this by attempting to adapt the fundamental technical notion of "model category" to directed topology.