如何证明教堂的编码，永远如此 F r-> r-> r，给出函子F的初始代数？

如何解决如何证明教堂的编码，永远如此 F r-> r-> r，给出函子F的初始代数？

众所周知的自然数的Church编码可以推广为使用任意仿函数F。结果是类型，称为C，由

定义

  data C = Cfix { run :: forall r. (F r -> r) -> r }

在下文中，为简单起见，我们将假设F是已定义的固定函子。

众所周知，类型C是函子F的固定点，并且C是初始F代数。例如，如果函子F a是由

定义的

 data F a b = Empty | Cons a b

然后，F a的固定点是[a]（a类型的值的列表）。同样，[a]是初始代数。列表的教堂编码是众所周知的。但是我找不到这些语句中任何一个的严格证明（C是一个固定点，C是初始代数）。

问题是，如何严格证明以下两种说法之一：

1. 类型C是同构类型F C ≅ C的固定点。换句话说，我们需要证明存在两个功能，fix :: F C -> C和unfix :: C -> F C，使得fix . unfix = id和unfix . fix = id。
2. 类型C是函子F的初始代数；也就是F-代数类别中的初始对象。换句话说，对于给出函数A的任何类型p :: F A -> A（即A是F代数），我们可以找到唯一的函数{ {1}}是F代数态。这意味着q :: C -> A必须符合法律q的规定。我们需要证明，给定q . fix = p . fmap q和A，这样的p存在并且是唯一的。

这两个语句不相等；但证明（2）暗示（1）。 （兰贝克定理说，初始代数是同构。）

函数q和fix的代码可以相对容易地编写：

unfix

给定一个功能 fix :: F C -> C fix fc = Cfix (forall r. \g -> g . fmap (\h -> h g) fc ) unfix :: C -> F C unfix c = (run c) (fmap fix) ，该功能p :: F A -> A的代码写为

q

但是，似乎很难直接证明函数 q :: C -> A q c = (run c) p ，fix，unfix满足所需的属性。我找不到完整的证明。

证明q是初始代数（即C是唯一的）比证明q容易吗？

在此问题的其余部分中，我将展示一些为证明fix . unfix = id而能采取的步骤。

仅通过使用给定的功能代码无法证明（1）或（2）。我们需要其他假设。与Yoneda身份相似，

fix . unfix = id

我们需要假设函数的代码是完全参数化的（没有副作用，没有特殊选择的值或固定类型），以便可以应用参数定理。因此，我们需要假设类型 forall r. (A -> r) -> F r ≅ F A,仅包含满足适当自然法则的类型C的函数。

参数定理为此类型签名提供了以下自然定律：对于任何类型forall r. (F r -> r) -> r和A，对于任何函数B和p :: F B -> A，函数{ {1}}必须满足方程式

f :: A -> B

使用本自然性法与适当选择的c :: forall r. (F r -> r) -> r和 c (f . p) = f . c (p . fmap f) ，可以表明，该组合物p是类型的某些功能f所必须等于{ {1}}。

但是，在证明上似乎不可能进一步取得进展；目前尚不清楚为什么该函数必须等于fix . unfix。

让我们临时定义函数C -> C：

\c -> (run c) fix

然后将我的结果写为

id

也可以显示m。

有待证明 m :: (F C -> C) -> C -> C m t c = (run c) t 。一旦证明了这一点，我们将证明fix . unfix = m fix 。

unfix . fix = fmap (m fix)的自然法则，m fix = id和F C ≅ C的不同选择赋予了奇怪的身份

c

但是我不知道如何从这个身份中得出p。