2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки





Начать новую тему Ответить на тему
 
 Изоморфизм двух типов
Сообщение25.03.2017, 14:39 
Заслуженный участник
Аватара пользователя


27/04/09
20017
Уфа
Изоморфны ли пустой тип (обозначим его $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]$. Уууу… Изоморфизм не доказан.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ 1 сообщение ] 

Модераторы: Toucan, maxal, Karan, PAV, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group