Могу ли я иметь «зависимый тип копродукта»?

Я читаю книгу HoTT, и у меня есть (возможно, очень наивный) вопрос о материалах в первой главе.

В этой главе вводится тип функции

$$f:A\to B$$ а затем обобщается ее зависимость от и это называется типом зависимой функции .$B$$x:A$ $$B:A\to\mathcal{U},\qquad g:\prod_{x:A}B(x)$$

Далее в главе вводится тип продукта а затем обобщается его, делая зависимым от и это называется типом зависимой пары .

$$f:A\times B$$ $B$$x:A$ $$B:A\to\mathcal{U},\qquad g:\sum_{x:A}B(x)$$

Я определенно могу видеть образец здесь.

Далее в главе вводится сопутствующий тип

$$f:A+B$$ и ... combobreaker ... не обсуждается зависимая версия этого типа.

Есть ли какое-то фундаментальное ограничение на это или это просто не имеет отношения к теме книги? В любом случае, кто-то может мне помочь с интуицией, почему функции и типы продуктов? Что делает эти два настолько особенными, что их обобщают на зависимые типы, а затем используют для построения всего остального?

Зависит сумма является общим обобщением как декартово произведение × B и копроизведением + B . Просто так получается, что книга HoTT вводит зависимую сумму путем обобщения A × B , потому что это не требует, чтобы булев тип был определен первым.$A \times B$ $A + B$$A \times B$

Копродукция - это частный случай зависимой суммы. Указанные типы и B , рассмотрим тип семьи Р : б о о л → U определяется P ( F L сек е ) = А и Р ( т г у е ) = B . Зависимая сумма ∑ b : b o o l P ( b ) эквивалентна A + $A$$B$$P : \mathtt{bool} \to \mathcal{U}$$P(\mathtt{false}) = A$$P(\mathtt{true}) = B$$\sum_{b : \mathtt{bool}} P(b)$$A + B$, Кстати, вы также можете получить как зависимый продукт ∏ b : b o o l P ( b ) .$A \times B$$\prod_{b : \mathtt{bool}} P(b)$

Вы спрашиваете, что особенного в продуктах и ​​типах функций. Есть много, много причин , почему и Π являются «необходимыми». С точки зрения логики, они необходимы, потому что они соответствуют ∃ и ∀ соответствием типа предложения (но это только сдвигает вопрос: «Почему ∃ и ∀ необходимы?»). С точки зрения теории категорий, Σ и Π необходимы , поскольку они являются левыми и правыми , сопряженный к замещению. Задайте более конкретный вопрос, если вы хотите узнать больше.$\sum$$\prod$$\exists$$\forall$$\exists$$\forall$$\sum$$\prod$

Я расскажу об этом более программно-разработчиком.

Вы говорите о типе копроизведения, чьи последние конструкторы могут ссылаться на предыдущие (который выглядит очень похоже на продукт, чьи последние поля могут ссылаться на предыдущие)? Это возможно в Agda после введения HIT (в версии 2.6.0):

-- Auxiliary definition: Nat
data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

-- The HIT I was talking about
data Int : Set where
  positive : Nat -> Int
  negative : Nat -> Int
  -- Note this constructor uses `positive` and `negative`.
  zeroPath : positive zero ≡ negative zero

Следуя этой статье , если ваша программа проверки типов проверяет определения, определенные с использованием синтаксиса, представленного на рисунке "(26)", я считаю, что довольно просто поддерживать "зависимые сопутствующие продукты".