4
$\begingroup$

Does there exist a faithful (bicartesian closed) functor $\operatorname F$ from the freely generated bicartesian closed category $\mathbf B$ to $\mathbf{Set}$? Preferably, $\mathbf B$ should contain exactly the objects, arrows and commuting diagrams required by a bicartesian closed category, and nothing else, but other reasonable definitions are also welcome.

Put another way: does the free generation of arrows in $\mathbf B$, restricted only by its bicartesian closed structure, produce more arrows than there are arrows in $\mathbf{Set}$?

$\endgroup$
5
  • 3
    $\begingroup$ Unless ${\bf B}$ fails to be small, the functor $$X\longmapsto \{g:U\to X|g\in{\bf Hom}_{\bf B}\},$$ $$f:X\to Y\longmapsto f\circ,$$ yields a faithful functor into ${\bf Set}$. Further, even if this category fails to be small in e.g. $ZFC$, we can shift to a universe-based setting and get what we need by restricting attention to a version of ${\bf B}$ inside a fixed universe and be good to go. $\endgroup$
    – Alec Rhea
    Commented Oct 27, 2023 at 14:51
  • 4
    $\begingroup$ What is a bicartesian closed category? What is a bicartesian closed functor? $\endgroup$ Commented Oct 27, 2023 at 17:17
  • $\begingroup$ Isn't $B$ just the category of finite sets? The objects that $B$ is required to contain are initial and terminal objects $0, 1$, then it has to be freely closed under finite products, coproducts, and exponentials. Since product distributes over coproduct, closure under finite products + coproducts produces exactly finite coproducts of copies of $1$, and the behavior of exponentials on two such objects is uniquely determined. Am I missing something? $\endgroup$ Commented Oct 27, 2023 at 19:43
  • 1
    $\begingroup$ @QiaochuYuan This other question, that I just asked, is partly an attempt to make precise sense of the present one (which, as you point out, seems a bit strange). $\endgroup$
    – Gro-Tsen
    Commented Dec 12, 2023 at 10:02
  • $\begingroup$ @TimCampion: a bicartesian closed category is a cartesian closed category with finite coproducts. (The corresponding notion of functor is then clear.) $\endgroup$
    – varkor
    Commented Jan 2 at 17:41

0

You must log in to answer this question.

Browse other questions tagged .