2
$\begingroup$

In Category with Family by Castellan et al., 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

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ 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. $\endgroup$
    – Trebor
    Jun 8, 2022 at 4:16

1 Answer 1

Reset to default
3
$\begingroup$

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 for details.

Improve this answer
$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.