<p>In <a href="https://www.cambridge.org/us/universitypress/subjects/mathematics/logic-categories-and-sets/introduction-higher-order-categorical-logic" rel="nofollow noreferrer">Introduction to Higher Order Categorical Logic</a> part 1, section 4, Lambek defines an adjunction between <span class="math-container">$\mathbf{Graph}$</span>, 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 <span class="math-container">$\mathbf{Graph}$</span> and the category <span class="math-container">$\mathbf{Bicart}$</span> of bicartesian closed categories and bicartesian closed functors between them? If so, let <span class="math-container">$\operatorname{F} : \mathbf{Graph} \to  \mathbf{Bicart}$</span> be the Free functor of that adjunction.</p>
<p>Let</p>
<ul>
<li><span class="math-container">$(* \to)^0 * $</span> denote the kind <span class="math-container">$* $</span>,</li>
<li><span class="math-container">$(* \to)^1 * $</span> denote the kind <span class="math-container">$* \to * $</span>,</li>
<li><span class="math-container">$(* \to)^2 * $</span> denote the kind <span class="math-container">$* \to * \to * $</span>,</li>
</ul>
<p>and so on. Further, for each <span class="math-container">$n \ge 0$</span>, let <span class="math-container">$g_n$</span> be a discrete graph with <span class="math-container">$n$</span> nodes. For each <span class="math-container">$n$</span>, do the types of kind <span class="math-container">$(* \to)^n * $</span>, and all polymorphic functions between them, form a category? Is this category (isomorphic to) <span class="math-container">$\operatorname{F} g_n $</span>?</p>
<p>Clarification due to popular demand, sorry for the late response. I define the types of <span class="math-container">$(* \to)^n * $</span> recursively starting from <span class="math-container">$n$</span> (uninhabited) type variables <span class="math-container">$a_1, a_2, … a_n$</span>, 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 <span class="math-container">$(* \to)^n * $</span>, where composition is substitution plus normalization.</p>

CC BY-SA 4.0
2023-11-25T23:13:25.407Z
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.
Andrej Bauer
CC BY-SA 4.0
2023-11-25T23:16:44.967Z
Found it, page 55.
Andrej Bauer
CC BY-SA 4.0
2023-11-29T21:28:05.213Z
"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?
Max New
CC BY-SA 4.0
2023-12-10T10:52:45.373Z
I second @MaxNew's question: please state explicitly what sort of calculus you're working with.
Andrej Bauer
<reference-request><type-theory><ct.category-theory>
Is the Category of $(* \to)^n *$-kinded types freely generated from the discrete graph with $n$ nodes?
Johan Thiborg-Ericson
# Is the Category of $(* \to)^n *$-kinded types freely generated from the discrete graph with $n$ nodes?

(Asked by: username_0 on 2023-11-23)

In [Introduction to Higher Order Categorical Logic](https://www.cambridge.org/us/universitypress/subjects/mathematics/logic-categories-and-sets/introduction-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.

Let

* $(\* \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.

**Tags:** reference-request, type-theory, ct.category-theory
> **Comments:**
> **username_1**: 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.  
> **username_1**: Found it, page 55.  
> **username_2**: "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?  
> **username_1**: I second @MaxNew's question: please state explicitly what sort of calculus you're working with.  

---

## 0 answers

