0
$\begingroup$

I am reading the book Introduction to Higher-Order Categorical Logic by Lambek and Scott, and have run across this inference rule when they define what they call the "conjunction calculus":

$$A \xrightarrow{\bigcirc_{A}}T$$

What does the operator $\bigcirc_{A}$ mean?

$\endgroup$

1 Answer 1

1
$\begingroup$

To quote Lambek and Scott (section 0.5) "An object $T$ of a category $\scr A$ is said to be a terminal object if for each object $A$ of $\scr A$ there is a unique arrow $\bigcirc_A:A\to T$."

So $T$ is a terminal object in a category and $\bigcirc_A$ is the unique arrow from $A$ to $T$.

$\endgroup$
2
  • $\begingroup$ Thanks! I referred to a different text for the category theory part, so it's a little inconvenient that I missed that. Is this common notation in category theory? $\endgroup$
    – Richard
    Apr 17, 2019 at 17:47
  • 1
    $\begingroup$ @Richard No, I've never seen it before. $!_A$ is pretty common. $\endgroup$ Apr 17, 2019 at 18:27

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .