Circle symbol for true logical statements?

Question

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?

Answer 1

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$.