Прежде всего, давайте разберемся в терминологии.
То, что вы называете 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 является ответом . Чтобы процитировать начало сообщения в блоге Майка Шульмана:
В этом посте я буду утверждать, что, улучшая предыдущую работу Awodey-Frey-Speight, (более высокие) индуктивные типы могут быть определены с использованием импредикативных кодировок с их полностью зависимыми принципами индукции - в частности, исключения во все семейства типов без каких-либо гипотезы об укорочении - в обычной (непредсказуемой) Книге HoTT без каких-либо дополнительных наворотов.
(Хотя (непредсказуемую) кодировку, которую вы получите, вряд ли можно назвать церковной кодировкой.)