一个参数化的过程，
A parameterization process, functorially
摘要：
本文研究了符号计算系统Kenzo和EAT中的参数化过程，并将其作为范畴框架中的一般构造。这个参数化过程从给定的规范开始，通过将参数作为新变量添加到某些操作中来构建参数化规范。给定一个参数化规格说明的模型，对参数的每个解释（称为参数）都提供了给定规格说明的模型。此外，在某些相关的终结性假设下，给定规格说明的参数和模型之间的这种对应关系是双射。本文证明了参数化过程是由函子提供的，随后的参数传递过程是由自然变换提供的。使用了各种范畴概念，主要是伴随函子，推出和松弛余极限。
英文摘要：
The parameterization process used in the symbolic computation systems Kenzo and EAT is studied here as a general construction in a categorical framework. This parameterization process starts from a given specification and builds a parameterized specification by adding a parameter as a new variable to some operations. Given a model of the parameterized specification, each interpretation of the parameter, called an argument, provides a model of the given specification. Moreover, under some relevant terminality assumption, this correspondence between the arguments and the models of the given specification is a bijection. It is proved in this paper that the parameterization process is provided by a functor and the subsequent parameter passing process by a natural transformation. Various categorical notions are used, mainly adjoint functors, pushouts and lax colimits.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
