心身医学科是看什么病

Question

What is the most basic set-based interpretation of dependent types that one can use as a basic model when learning dependent type theory? Indeed, one is easily unmotivated to read formal rules before understanding even one basic interpretation that would help make sense of the theory, yet I literally cannot find such for dependent types. In fact, some of the descriptions of an interpretation literally seem contradictory. It for example seems to me nlab here claims interpretation of $(x \colon A) \vdash B(x) \colon Type$ would be morphism $I(B) \to I(A)$, whereas nlab here claims interpretation of $\Gamma \vdash B \colon Type$ would be morphism $I(\Gamma,y \colon B) \to I(\Gamma)$. Thus even though I kind of assume that dependent sums could be disjoint unions and dependent products Cartesian products, I actually literally have no idea how the actual dependent types should be interpreted even as the most basic easy example.

For simply typed theory a basic interpretation for sets is highly easy: basic types are sets, contexts are Cartesian products, product types are Cartesian products, function types are Cartesian exponentials, term is function from its context to its type and defined inductively so that notably variables are projections and e.g. evaluation is given by evaluation of the Cartesian exponential and so on. Does there not exist easy extension of this to dependent types that would concretize things analogously?

Answer 1

The set-theoretic analogue of dependent types is indexed families of sets. If you think of types as being sets, then $(x:A)\vdash B(x):\text{Type}$ corresponds to the indexed family $(B_x)_{x\in A}$, where $A$ is a set and for each $x\in A$, $B_x$ is a set. Then the dependent product and sum correspond to the familiar operations of cartesian product and disjoint union of the indexed family.

The apparent contradictions in the interpretations you read probably come from two (superficially) different ways of formalizing the notion of indexed family of sets.

First, we could have a function $f\colon A\to V$, where $V$ is a class of sets, and define $B_x = f(x)$ for all $x\in A$.

Second, we could have a set $B$ and a function $g\colon B\to A$, and define $B_x = g^{-1}(\{x\})$ for all $x\in A$.

The first interpretation is more general than the second from the material set theory point of view, because in the second interpretation, the sets $B_x$ and $B_y$ are always disjoint when $x\neq y$. But from an isomorphism-invariant point of view, this is not a real restriction: any family of sets is isomorphic to one in which the sets are pairwise disjoint. And it turns out that the second interpretation often generalizes better to other settings.