David Corfield Arrow category

Idea

Logical constructions emerge via web of adjoints. A famous example is of product/conjunction and coproduct/disjunction as adjoints to duplication. But this can be factorised.

$$\mathcal{C}^{\; 2} \stackrel{\stackrel{p_1 \to p_1 + p_2}{\longrightarrow}}{\stackrel{\stackrel{(dom,cod)}{\longleftarrow}}{\stackrel{p_1 \times p_2 \to p_2}{\longrightarrow}}} \mathcal{C}^{\;\to} \stackrel{\stackrel{\cdot \to \ast}{\longleftarrow}}{ \stackrel{\stackrel{cod}{\longrightarrow}}{ \stackrel{\stackrel{id}{\longleftarrow}}{ \stackrel{\stackrel{dom}{\longrightarrow}}{ \stackrel{0 \to \cdot}{\longleftarrow} } } } } \mathcal{C}$$

$$\mathcal{C}^{\,2} \stackrel{\stackrel{p_1 \to p_1 + p_2}{\longrightarrow}}{\stackrel{\stackrel{(dom, cod)}{\longleftarrow}}{\stackrel{p_1 \times p_2 \to p_2}{\longrightarrow}}} \mathcal{C}^{\,\to} \stackrel{\stackrel{cod}{\longrightarrow}} {\stackrel{\stackrel{id}{\longleftarrow}}{\stackrel{dom}{\longrightarrow}}} \mathcal{C}$$

$$\mathcal{C}^{\,2} \stackrel{\stackrel{+}{\longrightarrow}}{\stackrel{\stackrel{\Delta}{\longleftarrow}}{\stackrel{\times}{\longrightarrow}}} \mathcal{C}$$

If we normally think of objects as types and arrows as terms, what about the arrow category? Here an object is a term and an object a morphism between terms.

How then to think of dependent sum as a right adjoint?

For a dependent type given by $p: B \to A$, we want $Hom_{\mathcal{C}}(C, B)$ to be equivalent to maps from $C$ to $A$ factoring through $p: B \to A$. So that’s maps in the arrow category $Arr(\mathcal{C})$ between $id_C: C \to C$ and $p: B \to A$.

So the negative presentation of dependent sum type is rendering the counit and Hom isomorphism of the domain cofibration as right adjoint to $Id: \mathcal{C} \to Arr(\mathcal{C})$.