Posso ter um "tipo de coproduto dependente"?

Estou lendo o livro do HoTT e tenho uma pergunta (provavelmente muito ingênua) sobre as coisas do capítulo um.

O capítulo apresenta o tipo de função e o generaliza, tornando B dependente de x : A B : A → U

$$f:A\to B$$ $B$$x:A$ e isso é chamado detipo de função dependente. $$B:A\to\mathcal{U},\qquad g:\prod_{x:A}B(x)$$

Seguindo em frente, o capítulo apresenta o tipo de produto e o generaliza, tornando B dependente de x : A B : A → U

$$f:A\times B$$ $B$$x:A$ e isso é chamado detipo de par dependente. $$B:A\to\mathcal{U},\qquad g:\sum_{x:A}B(x)$$

Definitivamente, posso ver um padrão aqui.

Seguindo em frente, o capítulo apresenta o tipo de coproduto e ... combobreaker ... não há discussão sobre a versão dependente desse tipo.

$$f:A+B$$

Existe alguma restrição fundamental sobre isso ou é apenas irrelevante para o tópico do livro? De qualquer forma, alguém pode me ajudar com a intuição sobre por que tipos de função e produto? O que torna esses dois tão especiais que eles podem ser generalizados para tipos dependentes e usados ​​para construir todo o resto?

A soma dependente é uma generalização comum de ambos o produto cartesiano e o co-produto A + B . Acontece que o livro HoTT introduz uma soma dependente generalizando A × B , porque isso não exige que o tipo booleano seja definido primeiro.$A \times B$ $A + B$$A \times B$

O coproduto é um caso especial de soma dependente. Dado tipos e B , considerar o tipo da família P : b S O l → L definido por P ( f um l s e ) = A e P ( t r u e ) = B . A soma dependente Σ b : b o o l P ( b ) é equivalente a um $A$$B$$P : \mathtt{bool} \to \mathcal{U}$$P(\mathtt{false}) = A$$P(\mathtt{true}) = B$$\sum_{b : \mathtt{bool}} P(b)$$A + B$. By the way, você também pode obter como um produto dependente Π b : b o o l P ( b ) .$A \times B$$\prod_{b : \mathtt{bool}} P(b)$

Você pergunta o que há de especial em produtos e tipos de funções. Existem muitas, muitas razões pelas quais e ∏ são "necessárias". Em termos de lógica, eles são necessários porque correspondem a ∃ e ∀ pela correspondência proposições como tipos (mas isso apenas muda a questão para "por que são ∃ e ∀ necessários?"). Em termos da teoria das categorias, ∑ e ∏ são necessários porque são os lados esquerdo e direito da substituição. Faça uma pergunta mais específica, se você quiser saber mais.$\sum$$\prod$$\exists$$\forall$$\exists$$\forall$$\sum$$\prod$

Vou falar sobre isso mais de engenharia de software.

Você está falando de um tipo de coproduto cujos últimos construtores podem se referir aos anteriores (que parecem muito com um produto cujos últimos campos podem se referir aos anteriores)? Isso é possível no Agda após a introdução do HIT (na versão 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

Seguindo este artigo , se o seu verificador de tipos verificar as definições definidas usando a sintaxe apresentada na figura "(26)", acredito que seja bastante simples oferecer suporte a "coprodutos dependentes".