<p>The way to get a &quot;free&quot; functor rather than an initial object is to allow the <span class="math-container">$\mathcal B$</span> in the category <span class="math-container">$\mathcal B$</span>-Scwfs to vary.</p>
<p>Then there is a forgetful functor <span class="math-container">$U$</span> from the category of Scwfs to the category of Sets that forgets everything except for the set of types. This has a left adjoint <span class="math-container">$F$</span>, where <span class="math-container">$F(\mathcal B)$</span> is the Scwf defined in Proposition 4.</p>
<p>This is an instance of a general equivalence between left adjoints and collections of initial objects in certain slice categories, see <a href="https://ncatlab.org/nlab/show/adjoint+functor" rel="nofollow noreferrer">the nlab</a> for details.</p>

CC BY-SA 4.0
2022-06-06T19:01:59.720Z
2022-06-06T19:01:59.720Z
Max New
<p>In <a href="https://arxiv.org/pdf/1904.00827.pdf" rel="nofollow noreferrer">Category with Family by Castellan et al.</a>, they introduce the concept of Free SCWF as correspondence of STLC with base type. Seemingly, they define Free B-SCWF as the synonym of initial B-SCWF.</p>
<p>My question is, since this is a &quot;free&quot; scwf, I thought there should be free and forgetful functors between the category of B-SCWF and something. Where can I find (the citation of) such adjoint functors?</p>
<p><a href="https://i.sstatic.net/ULpKe.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/ULpKe.png" alt="enter image description here" /></a></p>

CC BY-SA 4.0
2022-06-08T04:16:13.197Z
I would like to point out that, given **any** category $\mathcal C$ with initial object $0$, then the functor $F : \boldsymbol 1 \to \mathcal C$ mapping the one-object category to the initial object *is* the free functor, adjoint to $U : \mathcal C \to \boldsymbol1$. So in this sense the initial object is indeed free.
Trebor
<type-theory><lambda-calculus><ct.category-theory><typed-lambda-calculus>
Question about "Free-ness" of Free SCWF
EDJ
# Question about "Free-ness" of Free SCWF

(Asked by: username_0 on 2022-06-04)

In [Category with Family by Castellan et al.](https://arxiv.org/pdf/1904.00827.pdf), they introduce the concept of Free SCWF as correspondence of STLC with base type. Seemingly, they define Free B-SCWF as the synonym of initial B-SCWF.

My question is, since this is a "free" scwf, I thought there should be free and forgetful functors between the category of B-SCWF and something. Where can I find (the citation of) such adjoint functors?

[![enter image description here](https://i.sstatic.net/ULpKe.png)](https://i.sstatic.net/ULpKe.png)

**Tags:** type-theory, lambda-calculus, ct.category-theory, typed-lambda-calculus
> **Comments:**
> **username_1**: I would like to point out that, given **any** category $\mathcal C$ with initial object $0$, then the functor $F : \boldsymbol 1 \to \mathcal C$ mapping the one-object category to the initial object *is* the free functor, adjoint to $U : \mathcal C \to \boldsymbol1$. So in this sense the initial object is indeed free.  

---

## 1 answers

### Answer by username_2 on 2022-06-06. Score: 3 | Accepted answer

The way to get a "free" functor rather than an initial object is to allow the $\mathcal B$ in the category $\mathcal B$-Scwfs to vary.

Then there is a forgetful functor $U$ from the category of Scwfs to the category of Sets that forgets everything except for the set of types. This has a left adjoint $F$, where $F(\mathcal B)$ is the Scwf defined in Proposition 4.

This is an instance of a general equivalence between left adjoints and collections of initial objects in certain slice categories, see [the nlab](https://ncatlab.org/nlab/show/adjoint+functor) for details.


---

