Terminal objects are initial objects in the opposite category

[zwang123]

Not sure if this is provable or already proposed. Just an idea that terminal object could be potentially defined this way?

$$ \mathrm{TermO} = \mathrm{InitO} \circ \mathrm{oppCat} $$

(or provide it as a theorem)

Potentially adding this as well?

$$ \mathrm{InitO} = \mathrm{TermO} \circ \mathrm{oppCat} $$

[tirix]

It would be great to have more development in Category theory!

@avekens already has definitions of initial and terminal objects in his mathbox.
We tend to prefer to stick to textbook definitions whenever possible, and that's the case here.

In this case, the two statements you mention could be introduced as theorems.
These alternative definition theorems are usually labelled dfxxx2, like in ~ dffn2.

[avekens]

If somebody volunteers to prove these two theorems (alternate definitions), I would appreciate this. For this, the material in my mathbox can be moved to main.

[zwang123]

I might try... No guarantee on when it will be done though.

[zwang123]

I finished proving
|- TermO = ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) )

(Note that the original theorem I proposed was false because the domain of oppCat is _V.)

Now considering how to name the theorem...

Maybe dftermo2.

[tirix]

Maybe dftermo2.

Yes!

[benjub]

I copy from #4170 (comment) what I should have written here:

Actually, your dftermo2 should be the "official" definition, and we may make the change in a future PR. But, as you noticed, the variable-free definition does not work for the moment because of the domains. This is something we may want to fix first (simply by changing the domains of these functions).