From 13450c1d232f36b916f3d32aa6c9d3730fdf77f9 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Tue, 14 Nov 2023 20:23:32 +0100 Subject: [PATCH] Show that K is PreElgot --- src/Monad/Instance/K/PreElgot.lagda.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md index 45a4f74..44b20e4 100644 --- a/src/Monad/Instance/K/PreElgot.lagda.md +++ b/src/Monad/Instance/K/PreElgot.lagda.md @@ -11,9 +11,12 @@ module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK open Ambient ambient open MIK ambient open MonadK MK +open import Algebra.ElgotAlgebra ambient +open import Algebra.UniformIterationAlgebra ambient open import Monad.ElgotMonad ambient open import Monad.Instance.K ambient open import Monad.Instance.K.Compositionality ambient MK +open import Monad.Instance.K.Commutative ambient MK open Equiv open HomReasoning @@ -24,9 +27,14 @@ open M C # K is a pre-Elgot monad ```agda +open kleisliK using (extend) +-- TODO fix global declarations on Commutative.lagda.md +-- open Elgot-Algebra-on using (#-Compositionality) +_# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f + preElgot : IsPreElgot monadK preElgot = record { elgotalgebras = λ {X} → elgot X - ; assoc = {!!} + ; assoc = λ f h → sym (extend-preserve h f) } ```