1
$\begingroup$

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

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

Improve this question
$\endgroup$
7
  • $\begingroup$ 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. $\endgroup$
    – Trebor
    Jun 4, 2022 at 13:17
  • $\begingroup$ @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? $\endgroup$
    – EDJ
    Jun 4, 2022 at 13:33
  • $\begingroup$ @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? $\endgroup$
    – EDJ
    Jun 4, 2022 at 13:36
  • $\begingroup$ The book is already adding products. Why not do the same to coproducts? $\endgroup$
    – Trebor
    Jun 4, 2022 at 13:40
  • $\begingroup$ @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 $\endgroup$
    – EDJ
    Jun 4, 2022 at 13:42

1 Answer 1

Reset to default
2
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$
    – EDJ
    Jun 4, 2022 at 13:57
  • 2
    $\begingroup$ @EDJ No. There are no extra information. And this "no extra information" thing is the whole point of freeness. $\endgroup$
    – Trebor
    Jun 4, 2022 at 13:59

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.