型加细与monoidal闭双纤维化
Type refinement and monoidal closed bifibrations
摘要：
类型论中的精化概念是一种调和类型的“内在”和“外在”意义的方法。我们从这个概念的严格分析开始，得出一个简单的结论，即“类型精化系统”的类型理论概念可以与“函子”的范畴理论概念相一致。然后，我们使用这种对应关系，给出了一个等价的类型理论制定的Grothendieck的定义（双）纤维化，并将其扩展到定义的monoidal封闭bifibrations，我们认为这是一个自然的空间中，研究性质的证明和程序。我们的主要结果是一个表示定理强单子上的monoidal闭纤维化，描述了充分条件单子同构的延续单子“上拉回”。
英文摘要：
The concept of_refinement_ in type theory is a way of reconciling the "intrinsic" and the "extrinsic" meanings of types. We begin with a rigorous analysis of this concept, settling on the simple conclusion that the type-theoretic notion of "type refinement system" may be identified with the category-theoretic notion of "functor". We then use this correspondence to give an equivalent type-theoretic formulation of Grothendieck's definition of (bi)fibration, and extend this to a definition of_monoidal closed bifibrations_, which we see as a natural space in which to study the properties of proofs and programs. Our main result is a representation theorem for strong monads on a monoidal closed fibration, describing sufficient conditions for a monad to be isomorphic to a continuations monad "up to pullback".
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
