-- Proof that closure operators on Posets are equal to monads on the corresponding thin category
open import Poset

-- Proof that in a Category C induced by a total order T every monad is strong.
open import Toset