In Introduction to Higher Order Categorical Logic part 1, section 4, Lambek defines an adjunction between $\mathbf{Graph}$, the category of graphs and graph homomorphisms, and the category of Cartesian closed categories with a natural number object and Cartesian closed functors between them. Is there a similar adjunction between $\mathbf{Graph}$ and the category $\mathbf{Bicart}$ of bicartesian closed categories and bicartesian closed functors between them? If so, let $\operatorname{F} : \mathbf{Graph} \to \mathbf{Bicart}$ be the Free functor of that adjunction.


  • $(* \to)^0 * $ denote the kind $* $,
  • $(* \to)^1 * $ denote the kind $* \to * $,
  • $(* \to)^2 * $ denote the kind $* \to * \to * $,

and so on. Further, for each $n \ge 0$, let $g_n$ be a discrete graph with $n$ nodes. For each $n$, do the types of kind $(* \to)^n * $, and all polymorphic functions between them, form a category? Is this category (isomorphic to) $\operatorname{F} g_n $?

Clarification due to popular demand, sorry for the late response. I define the types of $(* \to)^n * $ recursively starting from $n$ (uninhabited) type variables $a_1, a_2, … a_n$, the initial and terminal objects defined as usual by the empty type and a one-value type, and all coproducts, products and exponentials freely combined from those base types. I guess the arrows have to be all simply typed lambda expressions in normal form, with types corresponding to the exponentials of $(* \to)^n * $, where composition is substitution plus normalization.

  • $\begingroup$ Could you point to the exact place in the book where this is done? I thought there was an adjunction between graphs and categories (ordinary ones, not ccc's), that's exercise 8 on page 16. $\endgroup$ Nov 25, 2023 at 23:13
  • 1
    $\begingroup$ Found it, page 55. $\endgroup$ Nov 25, 2023 at 23:16
  • 2
    $\begingroup$ "For each 𝑛, do the types of kind (∗→)𝑛∗, and all polymorphic functions between them, form a category" -- can you be more precise about what you mean by a "polymorphic function" and "types of kind ..."? Are you referring to a particular polymorphic lambda calculus e.g. System Fomega? $\endgroup$
    – Max New
    Nov 29, 2023 at 21:28
  • 1
    $\begingroup$ I second @MaxNew's question: please state explicitly what sort of calculus you're working with. $\endgroup$ Dec 10, 2023 at 10:52


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.