<p>If you start out with a graph <span class="math-container">$1 \rightrightarrows 2$</span>, then what you get is not the <span class="math-container">$2$</span> you'd expect. The result would be equivalent to (in the resulting logic):</p>
<pre><code>postulate
  A B : Set
  f g : A -&gt; B
</code></pre>
<p>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.</p>
<hr />
<p>If you <em>do</em> want the if-then-else thing, you should not modify <span class="math-container">$\mathscr X$</span>. 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.</p>

CC BY-SA 4.0
2022-06-04T13:57:26.657Z
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
CC BY-SA 4.0
2022-06-04T13:59:41.573Z
@EDJ No. There are no extra information. And this "no extra information" thing is the *whole point* of **freeness**.
Trebor
CC BY-SA 4.0
2022-06-04T13:55:48.333Z
2022-06-04T13:58:33.470Z
2022-06-04T13:58:33.470Z
Trebor
<p>In Lambek's <a href="https://books.google.ca/books?id=6PY_emBeGjUC&amp;pg=PA41&amp;source=gbs_toc_r&amp;cad=3#v=onepage&amp;q&amp;f=false" rel="nofollow noreferrer">Intro to Higher Order Cat Logic</a>, Chapter 1 Section 4 introduces the free construction (upon graph) <a href="https://i.sstatic.net/Q5QOn.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/Q5QOn.png" alt="enter image description here" /></a></p>
<p>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 &quot;1&quot; to a vertex &quot;2&quot;, but it seems to me that, this free construction will add a new terminal object into the resulting CCC and the vertex &quot;1&quot; doesn't necessary become the desired terminal object and thus I am still confused where do I have <code>tt, ff : 1 -&gt; 2</code></p>
<p>[3]: Thanks for Trebor's correction on the terminology, that shouldn't be a boolean type but a fake/incomplete boolean type</p>

CC BY-SA 4.0
2022-06-04T13:17:16.430Z
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.
Trebor
CC BY-SA 4.0
2022-06-04T13:33:58.477Z
@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
CC BY-SA 4.0
2022-06-04T13:36:03.370Z
@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
CC BY-SA 4.0
2022-06-04T13:40:00.960Z
The book is already adding products. Why not do the same to coproducts?
Trebor
CC BY-SA 4.0
2022-06-04T13:42:17.277Z
@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
CC BY-SA 4.0
2022-06-04T13:44:36.600Z
No. 2 **is** the coproduct 1 + 1, and this is a fact no matter how you formulate it. Without the universal property, there would be no such thing as "2". The best you can do is to manually add everything so as to avoid the phrase "universal property", but I don't consider it any more illuminating. You *can* just add **one coproduct** which is 1+1, **without adding anything else**.
Trebor
CC BY-SA 4.0
2022-06-04T13:54:18.640Z
@Trebor Thanks for the correction. I will avoid using some confusing phrase "2 without universal property" haha.  So what you mean is that, if I generate free CCC with graph { "A" ---two arrows--> "B" }, the elimination rule for coproduct  "B" won't appear with "B" right? or do you mean the elimination rule for coproduct will appear together with "B"
EDJ
<type-theory><lambda-calculus><ct.category-theory><typed-lambda-calculus>
Question in relating STLC and Free CCC
EDJ
# Question in relating STLC and Free CCC

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

In Lambek's [Intro to Higher Order Cat Logic](https://books.google.ca/books?id=6PY_emBeGjUC&pg=PA41&source=gbs_toc_r&cad=3#v=onepage&q&f=false), Chapter 1 Section 4 introduces the free construction (upon graph) [![enter image description here](https://i.sstatic.net/Q5QOn.png)](https://i.sstatic.net/Q5QOn.png)

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

**Tags:** type-theory, lambda-calculus, ct.category-theory, typed-lambda-calculus
> **Comments:**
> **username_1**: 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.  
> **username_0**: @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?  
> **username_0**: @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?  
> **username_1**: The book is already adding products. Why not do the same to coproducts?  
> **username_0**: @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  
> **username_1**: No. 2 **is** the coproduct 1 + 1, and this is a fact no matter how you formulate it. Without the universal property, there would be no such thing as "2". The best you can do is to manually add everything so as to avoid the phrase "universal property", but I don't consider it any more illuminating. You *can* just add **one coproduct** which is 1+1, **without adding anything else**.  
> **username_0**: @Trebor Thanks for the correction. I will avoid using some confusing phrase "2 without universal property" haha.  So what you mean is that, if I generate free CCC with graph { "A" ---two arrows--> "B" }, the elimination rule for coproduct  "B" won't appear with "B" right? or do you mean the elimination rule for coproduct will appear together with "B"  

---

## 1 answers

### Answer by username_1 on 2022-06-04. Score: 2

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.

> **Comments:**
> **username_0**: 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?  
> **username_1**: @EDJ No. There are no extra information. And this "no extra information" thing is the *whole point* of **freeness**.  

---

