The category of monoids has all colimits.

We do this construction knowing nothing about monoids. In particular, I want to claim that this file could be produced by a python script that just looks at the output of #print monoid:

-- structure monoid : Type u → Type u -- fields: -- monoid.mul : Π {α : Type u} [c : monoid α], α → α → α -- monoid.mul_assoc : ∀ {α : Type u} [c : monoid α] (a b c_1 : α), a * b * c_1 = a * (b * c_1) -- monoid.one : Π (α : Type u) [c : monoid α], α -- monoid.one_mul : ∀ {α : Type u} [c : monoid α] (a : α), 1 * a = a -- monoid.mul_one : ∀ {α : Type u} [c : monoid α] (a : α), a * 1 = a

and if we'd fed it the output of #print comm_ring, this file would instead build colimits of commutative rings.

A slightly bolder claim is that we could do this with tactics, as well.

Because this file is "pre-automated", it doesn't meet current documentation standards. Hopefully eventually most of it will be automatically synthesised.