is "theory of objects" 

One data type. Equational theory with no operations and axioms.

Просто теория штук. Теория множеств ее моделирует, понятное дело.

So, take an algebraic theory; we can build algebras - models of that theory, and a free algebra is a free model (e.g. free monoid); then we can also look at Kleisli category, and there we have a terminal object, and it's supposed to be as easily buildable as free algebras (if they exist).

That kindergarten should be translated back to a proper categorical language. Maybe even better, into toposes, because it's a pretty old story. 

 Geometric Model Theory - hard reading, manifolds, algebraic geometry
Model Theory and Category Theory - high level, but easy reading

Solving the mystery behind Abstract Algorithm’s magical optimizations - here the author implements, in lambda, algorithms with unusually fast performance. Explanations follow (links inside)

A link to the author's github project

Basically, I have two, e.g. GraphMorphisms, and I want to compare them. This theory is supposed to be equational, right? Is it?
In short, I could not figure out.

So I decide, let me take a look, how do they compare two typed sets in Scala? Here's how:

  override def equals(that: Any): Boolean = that match {
    case that: GenSet[_] =>
      (this eq that) ||
      (that canEqual this) &&
      (this.size == that.size) &&
      (try this subsetOf that.asInstanceOf[GenSet[A]]
       catch { case ex: ClassCastException => false })
    case _ =>
      false
  }

So there. Maybe it's not equational, after all. I mean, in my case.

How do they do it in Haskell then? This is how:

instance Eq1 Set where
    liftEq eq m n =
        size m == size n && liftEq eq (toList m) (toList n)

Typeclasses seem to beat classes. Fuck...

PMMP.ch7 

Comments, critique welcome

on one page

1. Idea

The theory of objects is the logical theory whose models in a category 𝒞 are precisely the objects of 𝒞.

2. Definition

The theory of objects 𝕆 is the theory with no axioms over the signature with a single type and no primitive symbols except equality.


===================

The classifying topos 𝒮[𝕆] for the theory of objects 𝕆, or the object classifier, as it is also called, is the presheaf topos [FinSet,Set] on the opposite category of FinSet.

What motivates the terminology, is that for any topos E, geometric morphisms E→𝒮[𝕆] correspond to objects of E.