Monadicity Theorems

Another short post to highlight the existence of an article about the Monadicity Theorems, in which I prove one direction of both the Crude and Precise versions. Comments and corrections would be very much appreciated, because there is an awful lot of work involved in proving those theorems. It would be good to know of any parts where the argument is unclear, unmotivated, too long-winded, or wrong.