要理解 Display map category 的定義（參考 Categorical Logic and Type Theory, Definition 10.4.1），我們需要理解它的動機跟捕捉問題的方式，因此我們要觀察一個個相繼式（我假設讀者已經熟練相繼式定義的類型論），並用範疇論（category theory）的語言重述。

在用相繼式描述類型論時，公式

表示 $\Gamma$ 可派生出類型 $A$。對於所有 $\Gamma$ 可派生的類型，我們用 $Ty(\Gamma)$ 表示，所以我們也會用 $A \in Ty(\Gamma)$ 來表示上面的相繼式。Display map category 捕捉的第一件事就是 contexts 構成一個 category，我們用 $\mathcal{C}$ 記號表示這個範疇，並且我們要求 $\mathcal{C}$ 有 terminal object $\diamond$，用來表示空的 context。

context 的構造方式只有兩種：$\diamond$ 是一個 context；context $\Gamma$ 加入一個類型 $A$ 得到的 $\Gamma \triangleright A$ 還是 context。

因此 $\Gamma \triangleright A \triangleright B \triangleright \cdots$ 也常被稱為 telescope

在相繼式中如果我們寫

我們的意思是 $\Delta = \diamond \triangleright T_1 \triangleright \cdots \triangleright T_k$，對於每一個 $T_i$，都能找到 $\sigma_i : T_i$，我們稱「$\sigma$ 實現了 $\Delta$」。

但上面那樣寫有問題，因為 $\sigma$ 沒有憑依，因此正確的通用寫法是記錄成

這表示 $\sigma$ 參考 $\Gamma$ 中的變數，並實現了 $\Delta$，這叫做一個替換。

而很明顯的，對於所有 $\Gamma = \diamond \triangleright T_1 \triangleright \cdots \triangleright T_k$ 有一個「引用變數 $\Gamma_i$ 來實現 $T_i$ 的不變替換 $id_\Gamma$」，所以我們想把每個替換 $\sigma$ 視為 $\mathcal{C}$ 中的 morphism $\sigma : \Gamma \to \Delta$。這裡需要證明幾件事

1. 對於給定的 $\Gamma, \Delta$，可能的 $\Gamma \to \Delta$ 的 collection 是一個集合。由於所有替換都涉及對 $\Gamma$ 的引用（或是有限多的類型生成規則）並做出一個有限構造，所以可以用歸納的方式比較，這讓證明是唯一的，因此這些替換是 set
2. 對 $f : \Gamma \to \Delta$ 來說有 $f \circ id_\Gamma = f = id_\Delta \circ f$。根據定義就知道了
3. 替換要有 associative $f \circ (g \circ h) = (f \circ g) \circ h$。這個不好證明，就我所知都是對規則進行 induction 得到（參考 Substitution Without Copy and Paste 的 §4.3）

現在我們要進入 Display map 的部分

到這裡我們發現，這個模型很好的捕捉了 syntactic categorical 的觀點，把類型論的句法特性都保留了下來。前面說過每個替換都有逆變，現在我們要證明逆變是一個 functor：

Proposition. 逆變是 functor [local-6]

對於任何 $\sigma : \Delta \to \Gamma$，我們把逆變看成 slice category 的函數 $\mathcal{C} / \Gamma \to \mathcal{C} / \Delta$，要檢查這是否是 functor，我們想要證明兩件事：保留 identity 且保留 composition。

Proof. [local-5]

套上 display maps 的規範，知道逆變會產出一個 pullback：

這直接證明了 $\sigma \circ \sigma^*(id) = \sigma$，所以 $\sigma^*(id) = id_\Delta$，表示 $\sigma^*$ 保留了 identity。

要證明 composition，可以用 pullbacks 的結合知道如果 $\sigma^*(f) \circ \sigma^*(g)$ 跟 $\sigma^*(f \circ g)$ 的頂點 up to isomorphism 是同一個，因此這兩個 morphism 是一樣的，證明了也保留 composition。因此每個替換誘導出的逆變都是 functor。 □

既然 $\sigma^*$ 是個 functor，那在 display map category 裡，我們可以用 $\sigma^*$ 的 right adjoint 表示 product，而且加上 Beck-Chevalley 條件：存在一個 natural isomorphism，讓我們可以把 product 用替換推來推去而不會變成不同的東西。

weak sum 同理，只是變成 $\sigma^*$ 的 left adjoint，同樣要有 Beck-Chevalley 條件保證 coproduct 可以被推來推去而不遺失。strong sum 則是把條件強化到 display maps 組合一定是 display map，這蘊含 weak sum 條件。

我們前面完全沒有提到 $\Gamma \vdash a = a : A$ 這種形式，而確實這是 display map categorical 方法的額外條件：weak equality 用 diagonal 的 left adjoint $Eq_{\pi_A}$ 表示，還是用 Beck-Chevalley 條件避免遺失。strong equality 規定 diagonal 是 display map，蘊含 weak equality。

對細節有興趣的讀者可以看 Paige Randall North 的 slide：Homotopical models of type theory

現在我們看到，display map category 除了捕捉 type theory 的 syntactic 特性，還可以用直觀的範疇論語言表述 type theory 的數種特徵，成功的讓我們用範疇論的觀點來檢視類型論。