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
$\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$
  • $\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 at 17:47
  • 1
    $\begingroup$ @Richard No, I've never seen it before. $!_A$ is pretty common. $\endgroup$ – Kevin Carlson Apr 17 at 18:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.