-- Proof that kleisli triples correspond to monads
open import ExtensionSystem