## § Categorical model of dependent types

• A closed type is interpreted as an object.
• A term is interpreted as a morphism.
• A dependent type upon $X$ is interpreted as an object of the slice category $C/X$.
• A dependent type of the form x: A |- B(x) is a type corresponds to morphisms f: B -> A, whose fiber over x: A is the type f^{-1}(x) = B(x).
• The dependent sum $\Sigma_{x : A} B(x)$ is given by an object in $Set/A$, the set $\cup_{a \in A} B_a$. The morphism is the morphism from $B_a \to A$ which sends an elements of $B_{a_1}$ to $a_1$, $,B_{a_2}$ to $a_2$ and so forth. The fibers of the map give us the disjoint union decomposition.
• The dependent product $\Pi_{x: A} A(x)$ is given by an object in $Set/A$.
• We can describe both dependent sum and product as arising as adjoints to the functor $Set \to Set/A$ given by $X \mapsto (X \times A \to A)$.
• Recalling that dependent types are interpreted by display maps, substitution of a term tt into a dependent type BB is interpreted by pullback of the display map interpreting BB along the morphism interpreting tt.

#### § Key ideas

• Contexts are objects of the category C
• Context morphisms are morphisms f: Γ → Δ
• Types are morphisms σ: X → Γ for arbitrary X
• Terms are sections of σ: X → Γ, so they are functions s: Γ → X such that σ . s = id(Γ)
• Substitution is pullback

#### § Why is substitution pullback?

• Suppose we have a function $f: X \to Y$, and we have a predicate $P \subseteq Y$.
• The predicate can be seen as a mono $P_Y \xrightarrow{py} Y$, which maps the subset where $P$ is true into $Y$.
• now, the subset $P_X \equiv P_Y(f(x))$, ie, the subset $P_X \equiv \{ x : f(x) \in P_Y \}$ is another subset $P_X \subseteq X$.
• See that $P_X$ is a pullback of $P$ along $f$:
P_X -univ-> P_Y
|            |
px            py
|            |
v            v
X -----f---> Y

• This is true because we can think of $Q_X \equiv \{ x \in X, y \in P_Y: f(x) = py(y) \}$.
• If we imagine a bundle, at each point $y \in Y$, there is the presence/absence of a fiber $py^{-1}(y)$since $py$ is monic.
• When pulling back the bundle, each point $x \in X$ either inherits this fiber or not depending on whether $f(x)$ has a fiber above it.
• Thus, the pullback is also monic, as each fiber of $px$ either has a strand or it does not, depending on whether $py$ has a strand or not.
• This means that $px(x)$ has a unique element precisely when $f(x)$ does.
• This means that $px$ is monic, and represents the subset that is given by $P_Y(f(x))$.

#### § Isn't substitution composition?

• If instead we think of a subset as a function $P_Y: Y \to \Omega$ where $\Omega$ is the subobject classifier, we then get that $P_X$ is the composite $P_X \equiv P_Y \circ f$.
• Similarly, if we have a "regular function" $f: X \to Y$, and we want to substitute $s(a)$ ( $s: A \to X$ for substitution) into $f(x)$ to get $f(s(a))$, then this is just computing $f \circ s$.

#### § Using this to do simply typed lambda calculus

• Judgement of the form A1, A2, A3 |- A becomes a morphism A1xA2xA3 → A.
• Stuff above the inference line will be arguments, stuff below the line will be the return value.
• Eg, the identity judgement:
Γ,A |- A

becomes the function snd: ΓxA → A.

#### § Display maps

• To to dependent types in a category, we can use display maps .
• The display map of a morphism $p: B \to A$ represents $x:A |- B(x): Type$. The intuition is that $B(x)$is the fiber of the map $p$ over $x:A$.
• For any category $C$, a class of morphisms $D$ are called display maps iff all pullbacks of $D$ exist and belong to $D$. Often, $D$ is also closed under composition.
• Said differently, $D$ is closed under all pullbacks, as well as composition.
• A category with displays is well rooted if the category has a terminal object $1$, and all maps into $1$are display maps (ie, they can always be pulled back along any morphism).
• This then implies that binary products exist (?? HOW?)