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

minor

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-15 14:37:28 +01:00
parent 344e08fc53
commit 0e89d52460
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 8 additions and 2 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

@ -17,6 +17,7 @@ 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 import Monad.Instance.K.Commutative ambient MK
open import Categories.FreeObjects.Free
open Equiv open Equiv
open HomReasoning open HomReasoning
@ -32,9 +33,14 @@ open kleisliK using (extend)
-- open Elgot-Algebra-on using (#-Compositionality) -- open Elgot-Algebra-on using (#-Compositionality)
_# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
preElgot : IsPreElgot monadK isPreElgot : IsPreElgot monadK
preElgot = record isPreElgot = record
{ elgotalgebras = λ {X} → elgot X { elgotalgebras = λ {X} → elgot X
; assoc = λ f h → sym (extend-preserve h f) ; assoc = λ f h → sym (extend-preserve h f)
} }
preElgot : PreElgotMonad
preElgot = record { T = monadK ; isPreElgot = isPreElgot }
-- initialPreElgot :
``` ```