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

🎨 Some more cleanup

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-18 11:49:19 +01:00
parent 50fee48b17
commit 7b39c02b12
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
3 changed files with 5 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Monad/Instance/K/Commutative.lagda.md
View file

@ -22,7 +22,7 @@ open import Category.Construction.UniformIterationAlgebras ambient
open import Algebra.UniformIterationAlgebra ambient open import Algebra.UniformIterationAlgebra ambient
open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra) open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
open import Algebra.ElgotAlgebra ambient open import Algebra.ElgotAlgebra ambient
open import Monad.Instance.K.Compositionality ambient MK open import Monad.Instance.K.Elgot ambient MK
open Equiv open Equiv
open HomReasoning open HomReasoning

6
src/Monad/Instance/K/Compositionality.lagda.md → src/Monad/Instance/K/Elgot.lagda.md
View file

@ -1,5 +1,3 @@
# TODO: every KX satisfies compositionality
```agda ```agda
{-# OPTIONS --allow-unsolved-metas #-} {-# OPTIONS --allow-unsolved-metas #-}
open import Level open import Level
@ -8,8 +6,10 @@ open import Category.Instance.AmbientCategory
import Monad.Instance.K as MIK import Monad.Instance.K as MIK
``` ```
# Every KX is a free Elgot algebra
```agda ```agda
module Monad.Instance.K.Compositionality {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where module Monad.Instance.K.Elgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
open Ambient ambient open Ambient ambient
open MIK ambient open MIK ambient
open MonadK MK open MonadK MK

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

@ -22,7 +22,7 @@ open import Algebra.ElgotAlgebra ambient
open import Algebra.UniformIterationAlgebra 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.Elgot ambient MK
open import Monad.Instance.K.Commutative ambient MK open import Monad.Instance.K.Commutative ambient MK
open import Monad.Instance.K.Strong ambient MK open import Monad.Instance.K.Strong ambient MK
open import Category.Construction.PreElgotMonads ambient open import Category.Construction.PreElgotMonads ambient
@ -37,11 +37,6 @@ open M C
# K is a pre-Elgot monad # K is a pre-Elgot monad
```agda ```agda
-- TODO fix global declarations on Commutative.lagda.md
-- open Elgot-Algebra-on using (#-Compositionality)
-- TODO fix this import mess!!!
-- _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
isPreElgot : IsPreElgot monadK isPreElgot : IsPreElgot monadK
isPreElgot = record isPreElgot = record
{ elgotalgebras = λ {X} → elgot X { elgotalgebras = λ {X} → elgot X
@ -52,7 +47,6 @@ isPreElgot = record
preElgot : PreElgotMonad preElgot : PreElgotMonad
preElgot = record { T = monadK ; isPreElgot = isPreElgot } preElgot = record { T = monadK ; isPreElgot = isPreElgot }
-- initialPreElgot :
initialPreElgot : IsInitial PreElgotMonads preElgot initialPreElgot : IsInitial PreElgotMonads preElgot
initialPreElgot = record initialPreElgot = record
{ ! = !′ { ! = !′