Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of the desired objects, but also "morphisms", which capture how different objects interact with each other. Category theory has found many applications in mathematics and in computer science, for example in functional programming. Double categories are a natural generalization of categories which incorporate the data of two separate classes of morphisms, allowing a more nuanced representation of relationships and interactions between objects. Similar to category theory, double categories have been successfully applied to various situations in mathematics and computer science, in which objects naturally exhibit two types of morphisms. Examples include categories themselves, but also lenses, petri nets, and spans. While categories have already been formalized in a variety of proof assistants, double categories have received far less attention. In this paper we remedy this situation by presenting a formalization of double categories via the proof assistant Coq, relying on the Coq UniMath library. As part of this work we present two equivalent formalizations of the definition of a double category, an unfolded explicit definition and a second definition which exhibits excellent formal properties via 2-sided displayed categories. As an application of the formal approach we establish a notion of univalent double category along with a univalence principle: equivalences of univalent double categories coincide with their identities

翻译：范畴论是数学的一个分支，它为理解数学结构之间的关系提供了形式化框架。为此，范畴不仅包含所研究对象的数椐，还包含"态射"，用以刻画不同对象之间的相互作用。范畴论在数学和计算机科学（例如函数式编程）中有着广泛应用。双范畴是范畴的自然推广，它包含两类独立态射的数椐，从而能够更细致地表示对象之间的关系和相互作用。与范畴论类似，双范畴已成功应用于数学和计算机科学中对象自然呈现两类态射的多种场景，例如范畴本身、透镜、佩特里网和跨距等。尽管范畴已在多种证明助手中得到形式化，但双范畴受到的关注却少得多。本文通过基于Coq证明助手和Coq UniMath库实现双范畴的形式化来弥补这一不足。作为本工作的一部分，我们提出了双范畴定义的两种等价形式化：一种展开的显式定义，和另一种通过双侧显示范畴展现优良形式性质的第二种定义。作为形式化方法的应用，我们建立了幺半双范畴概念以及幺半性原则：幺半双范畴的等价与其自身等同重合。