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.
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: