- Motivation for variants of categorical models of dependent types
- Seminal paper: Locally cartesian closed categories and type theory
- 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.
- Reference

- Intro to categorical logic
- 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

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

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

- Introduction to categories and categorical logic
- 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`

.
- Reference: Substitution on nlah
- 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?)