Изоморфны ли пустой тип (обозначим его

) и

в

? Если да, как показать часть

(

существует по определению пустого типа, откуда можно получить
![$g = \lambda(x\colon 0).\Lambda\alpha.o[\alpha]x\colon0\to\forall\alpha.\alpha$ $g = \lambda(x\colon 0).\Lambda\alpha.o[\alpha]x\colon0\to\forall\alpha.\alpha$](https://dxdy-04.korotkov.co.uk/f/b/7/5/b75425189719464a059e73ad025dba9b82.png)
).
-- Сб мар 25, 2017 16:53:39 --Какой я глупый.
![$f = \lambda(x\colon\forall\alpha.\alpha).x[0]$ $f = \lambda(x\colon\forall\alpha.\alpha).x[0]$](https://dxdy-04.korotkov.co.uk/f/7/b/3/7b356b69282fd61abd38cbf5922e5a6582.png)
же. Всё-таки изоморфны, и можно будет сегодня спать спокойно.
-- Сб мар 25, 2017 16:59:25 --Правда, остаётся показать, что

.
-- Сб мар 25, 2017 17:11:43 --![$f(gx) = (\Lambda\alpha.o[\alpha]x)[0] = o[0]x$ $f(gx) = (\Lambda\alpha.o[\alpha]x)[0] = o[0]x$](https://dxdy-03.korotkov.co.uk/f/a/c/a/aca0939aedc02f833da06df54863eb3582.png)
, а дальше ничего сделать нельзя.
![$(g(fx))[\alpha] = o[\alpha](x[0])$ $(g(fx))[\alpha] = o[\alpha](x[0])$](https://dxdy-01.korotkov.co.uk/f/0/8/e/08e591ce0e82ab2cf09f35cdbe2794e382.png)
, и тут тоже ничего сделать нельзя, а должны получиться соответственно

и
![$x[\alpha]$ $x[\alpha]$](https://dxdy-01.korotkov.co.uk/f/4/9/3/49350ec1eb7aa3dd9c21dc14a524325782.png)
. Уууу… Изоморфизм не доказан.