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

14

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

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

f:AB
а затем обобщается ее зависимость от и это называется типом зависимой функции .Bx:A
B:AU,g:x:AB(x)

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

f:A×B
Bx:A
B:AU,g:x:AB(x)

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

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

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

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

Костя
источник

Ответы:

18

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

Копродукция - это частный случай зависимой суммы. Указанные типы и B , рассмотрим тип семьи Р : б о о лU определяется P ( F L сек е ) = А и Р ( т г у е ) = B . Зависимая сумма b : b o o l P ( b ) эквивалентна A + BAВп:бооLUп(еaLsе)знак равноAп(TрUе)знак равноВΣб:бооLп(б)A+В, Кстати, вы также можете получить как зависимый продукт b : b o o l P ( b ) .A×ВΠб:бооLп(б)

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

Андрей Бауэр
источник
Здравствуйте. Могу ли я спросить, как вы можете показать, что « и присоединены слева и справа к замене»? Какие категории будут использоваться? ΣΠ
ChoMedit
Я предполагаю, что подстановка - это что-то вроде диагонального функтора, и работает в качестве его индексной категории. Тогда, возможно, предполагаемая категория - это категория типов. A
ChoMedit
1

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

Вы говорите о типе копроизведения, чьи последние конструкторы могут ссылаться на предыдущие (который выглядит очень похоже на продукт, чьи последние поля могут ссылаться на предыдущие)? Это возможно в 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)", я считаю, что довольно просто поддерживать "зависимые сопутствующие продукты".

ice1000
источник