Экзистенциальные типы: эквивалентность объектов

[Mysterious Light]

Рассматривается система Ж.И. Жирара с параметрическим полиморфизмом и типовыми операторами.
Пусть $F:*\to *$ — некий функтор (или просто типовый оператор)
Определим экзистенциальный тип $L = \forall \gamma(\forall \beta(F(\beta)\to\gamma)\to\gamma)$.
Пусть $g:L$. Произведём декомпозицию объекта: $g_\gamma (\Lambda\beta. \lambda h:F(\beta). \ldots)$.
Теперь на месте троеточия в контексте тех самых существующих $\beta$ и $h:F(\beta)$ воссоздадим объект $g$:

$$g' = g_{L} \big( \Lambda\beta. \, \lambda h:F(\beta).\, \Lambda\gamma.\, \lambda f:\forall\zeta(F(\zeta)\to\gamma). \, f_\beta h \big)$$

Интуиция и здравый смысл мне говорят, что если и не $g=g'$, то они хоть как-то должны быть связаны (мб, через изоморфизм).
Как бы это доказать? Можно делать любые удобные допущения, вроде экстенсиональности.

У Жирара, Душкина, Пирса, Барендрегта, Геверса ничего не обнаружил по этому вопросу.

-- Пн июл 04, 2016 21:05:20 --

Если предположить, что для некоторого типа $\Phi$ и некоторого терма $M:F(\Phi)$ выполняется

$$g=\Lambda\gamma. \; \lambda f:\forall\beta(F(\beta)\to\gamma). \; f_{F(\Phi)}M,$$

то всё доказывается прямолинейно. Но как быть в общем случае?

Я пробовал выписать бесплатную теорему для L, но не увидел, как из неё следует что-то полезное по этой задаче.

[Xaositect]

Mysterious Light в сообщении #1135733 писал(а):

Если предположить, что для некоторого типа $\Phi$ и некоторого терма $M:F(\Phi)$ выполняется

$$g=\Lambda\gamma. \; \lambda f:\forall\beta(F(\beta)\to\gamma). \; f_{F(\Phi)}M,$$

то всё доказывается прямолинейно.

А это разве не в точности то, что наш универсальный тип $\forall \gamma (\forall \beta (F\beta \to \gamma) \to \gamma)$ изоморфен экзистенциальному типу $\exists \beta . F\beta$? Я, честно говоря, не знаю, как это доказывается.

[Mysterious Light]

Xaositect в сообщении #1139834 писал(а):

Mysterious Light в сообщении #1135733 писал(а):

Если предположить, что для некоторого типа $\Phi$ и некоторого терма $M:F(\Phi)$ выполняется

$$g=\Lambda\gamma. \; \lambda f:\forall\beta(F(\beta)\to\gamma). \; f_{F(\Phi)}M,$$

то всё доказывается прямолинейно.

А это разве не в точности то, что наш универсальный тип $\forall \gamma (\forall \beta (F\beta \to \gamma) \to \gamma)$ изоморфен экзистенциальному типу $\exists \beta . F\beta$? Я, честно говоря, не знаю, как это доказывается.

В той литературе, которую я читал, можно выделить два подхода:
1. Экзистенциальный тип $\exists \beta. F\beta$ как синоним $\forall \gamma. (\forall \beta. F\beta\to\gamma)\to\gamma$.
2. Экзстенциальный тип как отдельная синтаксическая конструкция (например, Пирс «Типы в языках программирования») со своими introduction/exclusion правилами.

Мой вопрос звучит как-то так: почему, если мы распакуем объект и упакуем заново, мы получим то же самое. Какие условия достаточно наложить, чтобы после такой перепаковки мы получили в точности то, что имели.
Это как для пары $p=(\pi_1p,\pi_2p)$ — распаковали, упаковали, получили то же самое.

[Xaositect]

Я нашел нужное утверждение (о том, что любой терм экстенсионально равен упаковке $\Lambda\gamma . \lambda f\colon\forall\beta(F\beta\to\gamma) . f_{FX} x$, в статье "A logic for parametric polymorphism", параграф 3.3.

[Mysterious Light]

Большое спасибо!
Это как раз то, что я искал.