Изоморфизм двух типов

[arseniiv]

Изоморфны ли пустой тип (обозначим его $0$) и $\forall\alpha.\alpha$ в $\lambda2$? Если да, как показать часть $f\colon(\forall\alpha.\alpha)\to0$ ($o\colon\forall\alpha.0\to\alpha$ существует по определению пустого типа, откуда можно получить $g = \lambda(x\colon 0).\Lambda\alpha.o[\alpha]x\colon0\to\forall\alpha.\alpha$).

-- Сб мар 25, 2017 16:53:39 --

Какой я глупый. $f = \lambda(x\colon\forall\alpha.\alpha).x[0]$ же. Всё-таки изоморфны, и можно будет сегодня спать спокойно.

-- Сб мар 25, 2017 16:59:25 --

Правда, остаётся показать, что $f\circ g = \mathrm{id}, g\circ f = \mathrm{id}$.

-- Сб мар 25, 2017 17:11:43 --

$f(gx) = (\Lambda\alpha.o[\alpha]x)[0] = o[0]x$, а дальше ничего сделать нельзя.
$(g(fx))[\alpha] = o[\alpha](x[0])$, и тут тоже ничего сделать нельзя, а должны получиться соответственно $x$ и $x[\alpha]$. Уууу… Изоморфизм не доказан.