装饰的范畴论处理

装饰旨在驯服依赖类型理论中专用数据类型的大量衍生。在其原始形式中，装饰的定义与一个特定的数据类型宇宙紧密相连。作为一个类型论对象，装饰上的构造通常通过操作性的叙述来解释。这种过度的具体性要求一个抽象的装饰模型。在本文中，我们给出了装饰的范畴论模型。作为必要的第一步，我们使用多项式函子理论抽象了数据类型宇宙。然后，我们能够将装饰刻画为多项式函子之间的笛卡尔态射。由此，我们获得了强大的数学工具，这将有助于我们理解和发展装饰。我们还将说明我们模型的充分性。首先，我们将标准的装饰构造用我们的框架重新表述。得益于其简洁性，这一过程使我们对所涉及的结构有了更深入的理解。其次，通过将范畴结构转化为类型论构件，我们发展了新的装饰构造。