Lawvere理论与Jf-相对单子

在本文中，我们给出了 Lawvere 理论范畴与在明显函子 $Jf:F\rightarrow Sets$ 上的相对单子范畴之间等价性的详细构造，其中 $F$ 是以对象集 ${\bf N}$ 为对象集、态射为对应基数的标准有限集之间的函数的范畴。本文的方法是完全构造性的，并且应可在不含选择公理和排中律的 Zermelo-Fraenkel 集合论中形式化。它也容易在 UniMath 中形式化。