Kraus 悖论的范畴论表述

我们给出 Kraus' "magic trick" 用于从截断类型中恢复信息的范畴论表述。我们不使用类型论，而是使用 Van den Berg-Moerdijk 路径范畴，搭配单一宇宙，并不使用命题截断，而是使用任意单射，这包括截断作为一种特殊情况。我们使用 Kraus 的论证表明，任何具有齐次域的单射都是单态。我们给出一些在群块中说明齐次类型、单射和单值纤维之间相互作用的简单具体例子。