线性等式证明的等式性
Equality of Proofs for Linear Equality
摘要：
本文讨论了除合取命题和常真命题外，还用二元谓词形式化等式性质的等式证明问题。所讨论的等式的性质是预序关系的性质、等价关系的性质以及线性逻辑中适合于等式关系的其他性质。其指导思想是证明的平等性是由连贯性引起的，连贯性被理解为存在一个忠实函子，从一个句法范畴到一个其箭头对应于图的范畴。这些图中的边连接变量的出现，这些变量在证明的每个推广中必须保持不变。结果发现，平等的证明平等的假设是平行的标准假设的平等箭头的类别。它们在不同的层面上再现了标准的范畴假设。还发现，预序关系的假设涉及伴随的情况。
英文摘要：
This paper is about equality of proofs in which a binary predicate formalizing properties of equality occurs, besides conjunction and the constant true proposition. The properties of equality in question are those of a preordering relation, those of an equivalence relation, and other properties appropriate for an equality relation in linear logic. The guiding idea is that equality of proofs is induced by coherence, understood as the existence of a faithful functor from a syntactical category into a category whose arrows correspond to diagrams. Edges in these diagrams join occurrences of variables that must remain the same in every generalization of the proof. It is found that assumptions about equality of proofs for equality are parallel to standard assumptions about equality of arrows in categories. They reproduce standard categorial assumptions on a different level. It is also found that assumptions for a preordering relation involve an adjoint situation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
