Черч-кодирование зависимой пары

Прежде всего, давайте определимся с терминологией.

То, что вы называете dprod, на самом деле является «зависимой суммой», а «зависимый продукт» — это то, что у вас может возникнуть соблазн назвать «зависимой функцией». Причина этого в том, что зависимые функции обобщают обычные продукты, вам нужно только с умом использовать Bool:

prod : Set -> Set -> Set
prod A B = (b : Bool) -> case b of { True -> A; False -> B; }
{-
The type-theoretic notation would be:
prod A B = Π Bool (\b -> case b of { True -> A; False -> B; })
-}

mkPair : (A B : Set) -> A -> B -> prod A B
mkPair A B x y = \b -> case b of { True -> x; False -> y; }

elimProd : (A B Z : Set) -> (A -> B -> Z) -> prod A B -> Z
elimProd A B Z f p = f (p True) (p False)

В том же духе зависимые пары (обычно обозначаемые Σ) обобщают обычные суммы:

sum : Set -> Set -> Set
sum A B = Σ Bool (\b -> case b of { True -> A; False -> B; })

mkLeft : (A B : Set) -> A -> sum A B
mkLeft A B x = (True, x)

mkRight : (A B : Set) -> B -> sum A B
mkRight A B y = (False, y)

elimSum : (A B Z : Set) -> (A -> Z) -> (B -> Z) -> sum A B -> Z
elimSum A B Z f _ (True, x) = f x
elimSum A B Z _ g (False, y) = g y

Это может сбивать с толку, но, с другой стороны, Π A (\_ -> B) — тип обычных функций, а Σ A (\_ -> B) — тип обычных пар (см., например, здесь).

Итак, еще раз:

• Зависимый продукт = тип зависимых функций
• Зависимая сумма = тип зависимых пар

Ваш вопрос можно перефразировать следующим образом:

Существует ли Черч-кодирование для зависимых сумм через зависимые произведения?

Об этом уже спрашивали ранее на Math.StackExchange, и вот ответ, который дает практически ту же кодировку, что и ваша. .

Однако, читая комментарии к этому ответу, вы заметите, что в нем явно отсутствует ожидаемый принцип индукции. Существует также аналогичный вопрос, но относительно церковного кодирования натуральных чисел и этого ответа (в частности, комментариев) вроде объясняет, почему Coq или Agda недостаточно для вывода принципа индукции, вам нужны дополнительные предположения, такие как параметричность. Есть еще один похожий вопрос на MathOverflow, и хотя ответы не дают определенного «да» или «нет» для конкретного случая Agda/Coq, они подразумевают, что это, вероятно, невозможно.

Наконец, я должен упомянуть, что, как и многие другие вопросы теории типов в наши дни, по-видимому, HoTT — это ответ. Процитирую начало сообщения в блоге Майка Шульмана:

В этом посте я буду утверждать, что, улучшая предыдущую работу Аводи-Фрея-Спейта, (более высокие) индуктивные типы могут быть определены с использованием непредикативных кодировок с их принципами полной зависимой индукции - в частности, исключая во все семейства типов без каких-либо гипотез усечения - в обычном (непредикативном) Book HoTT без дополнительных наворотов.

(Хотя (непредикативное) кодирование, которое вы получите, вряд ли можно назвать кодированием Черча.)

В Coq или Agda невозможно закодировать зависимые пары по Черчу.

Хорошо, когда мы думаем об однородных кортежах AxA, это также можно понимать как функцию 2 -> A. Это также работает для разнородных кортежей, таких как AxB, с использованием зависимых функций Pi x:2.if x then A else B. Однако следующим логическим шагом является Sigma x:A.B x, которые не имеют хороших представлений в виде функций (если только мы не принимаем очень зависимые функции, что, на мой взгляд, противоречит духу теории типов). По этой причине мне кажется, что обобщение от -> до Pi и от x до Sigma первично, а тот факт, что кортежи могут быть представлены как функции, вторичен. -- Д-р Торстен Альтенкирх, где-то в списке рассылки Agda

Кодирование очень зависимых функций, о которых упоминает Торстен, можно найти здесь (примечание что это не действительный Agda, просто Agda-подобный синтаксис «безумно зависимой» теории типов).