In the paper The shift functor and the comprehensive factorization for internal groupoids by Bourn, the author proves that for a fixed finitely complete category, the category of internal groupoids is monadic over the category of points. The latter is the category whose objects are split epis equipped with a section, and whose arrows are serially commutative squares between such pairs.
The author notes this result is unexpected to him on page 2.
I am only able to follow parts of the proof and feel I am missing the big picture entirely. It just feels like black magic.
- How to think of this result? What is some intuition for it?
- What are the idea behind the proof?