leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Show that K is PreElgot

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-14 20:23:32 +01:00
parent 5641cb3dd7
commit 13450c1d23
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Monad/Instance/K/PreElgot.lagda.md
View file

@ -11,9 +11,12 @@ module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK
open Ambient ambient open Ambient ambient
open MIK ambient open MIK ambient
open MonadK MK open MonadK MK
open import Algebra.ElgotAlgebra ambient
open import Algebra.UniformIterationAlgebra ambient
open import Monad.ElgotMonad ambient open import Monad.ElgotMonad ambient
open import Monad.Instance.K ambient open import Monad.Instance.K ambient
open import Monad.Instance.K.Compositionality ambient MK open import Monad.Instance.K.Compositionality ambient MK
open import Monad.Instance.K.Commutative ambient MK
open Equiv open Equiv
open HomReasoning open HomReasoning
@ -24,9 +27,14 @@ open M C
# K is a pre-Elgot monad # K is a pre-Elgot monad
```agda ```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 : IsPreElgot monadK
preElgot = record preElgot = record
{ elgotalgebras = λ {X} → elgot X { elgotalgebras = λ {X} → elgot X
; assoc = {!!} ; assoc = λ f h → sym (extend-preserve h f)
} }
``` ```