# Question in relating STLC and Free CCC

In Lambek's Intro to Higher Order Cat Logic, Chapter 1 Section 4 introduces the free construction (upon graph)

My question is, if I want to have STLC + (fake/incomplete) boolean type, how do I have the corresponding category? One suggestion I was given is to generate upon two arrows from a vertex "1" to a vertex "2", but it seems to me that, this free construction will add a new terminal object into the resulting CCC and the vertex "1" doesn't necessary become the desired terminal object and thus I am still confused where do I have tt, ff : 1 -> 2

[3]: Thanks for Trebor's correction on the terminology, that shouldn't be a boolean type but a fake/incomplete boolean type

• That's multiple questions. As for the first question, it is obviously meant that 1 is the terminal object. Or more directly, that the coproduct 1+1 (but not necessarily the other coproducts) exists. Commented Jun 4, 2022 at 13:17
• @Trebor Thanks for quick feedback! Do you mind elaborate that? Because in my understanding, the free construction will have a new T(==1) added inside the resulting CCC, the old 1' from the graph doesn't seem to be related to the new T? Do you mean that they are iso?
– EDJ
Commented Jun 4, 2022 at 13:33
• @Trebor Also why is that a coproduct because I didn't meant to impose the if rules (the elimination for the vertex "2")? Do the universal property just also appear together at the end?
– EDJ
Commented Jun 4, 2022 at 13:36
• The book is already adding products. Why not do the same to coproducts? Commented Jun 4, 2022 at 13:40
• @Trebor This is just my small example, I intend to just add 2 without universal property. I am more curious on the "reaction" of the free construction and if I cannot control what is added and what is not added then I will need to be extra cautious about this concept
– EDJ
Commented Jun 4, 2022 at 13:42

If you start out with a graph $$1 \rightrightarrows 2$$, then what you get is not the $$2$$ you'd expect. The result would be equivalent to (in the resulting logic):

postulate
A B : Set
f g : A -> B


So you equivalently added two types (two propositions, two sets, whatever), and that there are two functions. But you don't get the case distinction (a.k.a. if-then-else) for the Boolean type.

If you do want the if-then-else thing, you should not modify $$\mathscr X$$. Rather, you should modify the free generation process. In the book you first put in a 1, and then add products, and add all the arrows resulting from universal properties. So you just sneak in an extra object 2 when you put in the 1, and add all the arrows together with the universal properties.

• Do I even have one element from the CCC unit to this A? i.e. , A closed element of A, and thus two closed element of B?
– EDJ
Commented Jun 4, 2022 at 13:57
• @EDJ No. There are no extra information. And this "no extra information" thing is the whole point of freeness. Commented Jun 4, 2022 at 13:59