module ФОРМАЛИЗУЕМ_ИЗОМОРФИЗМ_КАРРИ-ГОВАРДА_В_AGDA where

{-
Это интерактивная страничка: по вещам можно клацать

То, чем мы будем сегодня заниматься довольно забавно, потому что Agda сама по
себе уже основана на изоморфизме Карри - Говарда. То есть,
мы будем доказывать изоморфизм Карри-Говарда используя изоморфизм Карри-Говарда.

Хотя, конечно, в учебных целях для моделирования это полезно, да.

Предполагается, что читатель знаком с основными идеями и синтаксисом Agda.
Способы установки Agda, равно как и вещи вроде "Σ это ∃ и наоборот"
не обьясняются.

Сначала я сделал все нормально, но потом переписал все по-русски, мне кажется это интересный эксперимент.

-}

open import Вспомогательные_определения
open import Интуиционистское_Исчисление_Высказываний
open import Просто_типизированное_лямбда_исчисление
open import Изоморфизм_Карри-Говарда


{-
Все опеределения я придумал, основываясь на замечательной книжке
Lectures on the Curry-Howard Isomorphism (Sørensen, Urzyczyn).
Формализовывать ее на Агде оказалось проще, чем казалось
(не считая например известных сложностей с подстановкой
(которая не завершается) и устранением абстракции
(которая не вполне ясно определена)).

Дальнейшая работа по формализации Лекций ведется мной в силу
скромных умений в следующем репозитории
https://github.com/zelinskiy/NAL/tree/master/Examples/LCHI

Стандартную библиотеку Agda (если у вас ее нет) можно взять тут
https://github.com/agda/agda-stdlib/

Нашу версию изоморфизма можно расширить, добавив новые логические связки
и ⊥ в Φ и конструкций вроде пары и case в Λ.
-}