In order to round out our monadicity theorem collection, it would be fun to prove Duskin's Monadicity Theorem. There are a couple of variantions on this, but the following version seems the most elegant:

A conservative right adjoint U: D → C between finitely complete categories is monadic if any congruence in D which has a quotient in C already has a quotient in D, and that quotient that is preserved by U.