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

14

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 .

f : A \to B

$f:A\to B$

B

$B$

x : A

$x:A$

B : A \to U, g : \prod_{x : A} B (x)

$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 .

f : A \times B

$f:A\times B$

B

$B$

x : A

$x:A$

B : A \to U, g : \sum_{x : A} B (x)

$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

$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?

type-theory dependent-types homotopy-type-theory

— Kostya
źródło

18

$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$

— Andrej Bauer
źródło

\sum

$\sum$

\prod

$\prod$

A

$A$

1

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.

— ice1000
źródło