I would love love love to fix my first year course so we start with spuds-and-lemons gcd, and end with unification.
@pigworker Sounds like a good opportunity to mention the Stern-Brocot tree as well.
@leon_p_smith Stranger things have happened.

@pigworker I am very curious about the analogy between unification and gcd in your mind, though, as I personally haven't connected those two concepts.

(I'll admit I almost certainly don't have a particularly deep understanding of unification or why it's interesting... I just tend to resort to it typically as a strategy for solving problems by hand.)

@leon_p_smith Every monoid (multiplication of numbers or substitution of terms) induces a slice category ("this is a multiple of that" or "this is an instance of that") which raises the question of whether those slice categories have products, i.e. whether the original monoids have pullbacks ("this is the greatest common divisor" or "this is the most general unifier").

@pigworker Certainly an intriguing trail of breadcrumbs. I tried (and mostly failed) to understand Category Theory as an undergrad. Actually, I've been thinking about exact sequences a bit lately, and they are almost starting to make sense, and as a result category theory is almost starting to make sense as well.

... I don't know how many students need to start looking at exact sequences to start appreciating category theory. That would certainly be well outside the bounds of your class, but I'd love to take it, I'm sure I'd learn a lot!

@pigworker Thinking things over a bit this morning, I think I see (sort of) how things are supposed to go.

(Also, adding unification to my map of ideas surrounding the Stern-Brocot tree much too intriguing and important trailhead to pass up... this almost certainly needs to be incorporated into my notes, at least once I understand it better.)

There are clearly details I don't understand, but I was trying to think about pullbacks in the context of the subgroups of Z in the category of groups.

This is... not a great starting point, as all subgroups of Z are isomorphic to each other. But even my imperfect thinking here, I think I can see why unification and gcd could be connected.

And it has, I think, helped rectify some of my past misunderstandings about category theory; traditional abstract algebra often treats isomorphisms very blitheIy, and I think I have been missing something in the "sense and reference" interpretation of what a group "is".

Clearly I need to change my category, and/or particular objects I'm looking at, to arrive at an understanding of a useful result.