David Corfield Arrow category

Idea

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.

π’ž 2⟢p 1Γ—p 2β†’p 2⟡(dom,cod)⟢p 1β†’p 1+p 2π’ž β†’βŸ΅0β†’β‹…βŸΆdom⟡id⟢codβŸ΅β‹…β†’*π’ž \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}
π’ž 2⟢p 1Γ—p 2β†’p 2⟡(dom,cod)⟢p 1β†’p 1+p 2π’ž β†’βŸΆdom⟡id⟢codπ’ž \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}
π’ž 2βŸΆΓ—βŸ΅Ξ”βŸΆ+π’ž \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β†’Ap: B \to A, we want Hom π’ž(C,B)Hom_{\mathcal{C}}(C, B) to be equivalent to maps from CC to AA factoring through p:Bβ†’Ap: B \to A. So that’s maps in the arrow category Arr(π’ž)Arr(\mathcal{C}) between id C:Cβ†’Cid_C: C \to C and p:Bβ†’Ap: 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:π’žβ†’Arr(π’ž)Id: \mathcal{C} \to Arr(\mathcal{C}).

Last revised on June 23, 2023 at 05:19:37. See the history of this page for a list of all contributions to it.