A Universe of Sorts

§ Categorical model of dependent types

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

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