Czy mogę mieć „zależny typ koproduktu”?

Czytam poprzez książki hott i mam (prawdopodobnie bardzo naiwne) pytanie o rzeczy w jednym rozdziale.

Rozdział wprowadza typ funkcji a następnie uogólnia ją, uzależniając od i to się nazywa typ funkcji zależnej .B x : A B : A → U

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

Przechodząc dalej, rozdział wprowadza następnie typ produktu a następnie uogólnia go, uzależniając od i to się nazywa typ pary zależnej .B x : A B : A → U

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

Zdecydowanie widzę tutaj wzór.

Przechodząc dalej, rozdział wprowadza typ koproduktu i ... combobreaker ... nie dyskutuje się o zależnej wersji tego typu.

$$f:A+B$$

Czy są jakieś zasadnicze ograniczenia w tym względzie, czy jest to po prostu nieistotne dla tematu książki? W każdym razie ktoś może mi pomóc z intuicją, dlaczego typy funkcji i produktów? Co sprawia, że ​​te dwa są tak wyjątkowe, że można je uogólnić na typy zależne, a następnie wykorzystać do zbudowania wszystkiego innego?

$A \times B$ $A + B$$A \times B$

$A$$B$$P : \mathtt{bool} \to \mathcal{U}$$P(\mathtt{false}) = A$$P(\mathtt{true}) = B$$\sum_{b : \mathtt{bool}} P(b)$$A + B$$A \times B$$\prod_{b : \mathtt{bool}} P(b)$

$\sum$$\prod$$\exists$$\forall$$\exists$$\forall$$\sum$$\prod$

Opowiem o tym bardziej o inżynierii oprogramowania.

Czy mówisz o typie koproduktu, którego ostatni konstruktor może odnosić się do poprzednich (który wygląda dość podobnie do produktu, którego ostatnie pola mogą odnosić się do poprzednich)? Jest to możliwe w Agdzie po wprowadzeniu HIT (w wersji 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

Postępując zgodnie z tym artykułem , jeśli moduł sprawdzania typu sprawdza definicje zdefiniowane przy użyciu składni przedstawionej na rysunku „(26)”, uważam, że obsługa „zależnych koproduktów” jest dość prosta.