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

fix imports

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-20 09:25:52 +01:00
parent 1f4e5460d7
commit d762e280ad
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
4 changed files with 8 additions and 8 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.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
open import Algebra.ElgotAlgebra ambient
open import Monad.Instance.K.Elgot ambient MK
open import Monad.Instance.K.ElgotAlgebra ambient MK
open Equiv
open HomReasoning

2
src/Monad/Instance/K/Elgot.lagda.md → src/Monad/Instance/K/ElgotAlgebra.lagda.md
View file

@ -9,7 +9,7 @@ import Monad.Instance.K as MIK
# Every KX is a free Elgot algebra
```agda
module Monad.Instance.K.Elgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
module Monad.Instance.K.ElgotAlgebra {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
open Ambient ambient
open MIK ambient
open MonadK MK

4
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 Monad.PreElgot ambient
open import Monad.Instance.K ambient
open import Monad.Instance.K.Elgot ambient MK
open import Monad.Instance.K.ElgotAlgebra ambient MK
open import Monad.Instance.K.Commutative ambient MK
open import Monad.Instance.K.Strong ambient MK
open import Category.Construction.PreElgotMonads ambient
@ -34,7 +34,7 @@ open MR C
open M C
```
# K is a pre-Elgot monad
# K is the initial (strong) pre-Elgot monad
```agda
isPreElgot : IsPreElgot monadK

8
src/index.lagda.md
View file

@ -70,7 +70,7 @@ open import Monad.Instance.K.Strong
The next step is to show that every *KX* satisfies compositionality, meaning that each *KX* is an Elgot algebra.
```agda
open import Monad.Instance.K.Compositionality
open import Monad.Instance.K.ElgotAlgebra
```
and with this we can show that K is and equational lifting monad, i.e. a commutative monad satisfying the equational lifting law:
@ -80,9 +80,9 @@ open import Monad.Instance.K.Commutative
open import Monad.Instance.K.EquationalLifting
```
and lastly we formalize the notion of *pre-Elgot monad* and show that **K** is pre-Elgot.
and lastly we formalize the notion of *pre-Elgot monad* and show that **K** is the initial pre-Elgot monad.
```agda
open import Monad.ElgotMonad
-- open import Monad.Instance.K.PreElgot TODO
open import Monad.PreElgot
open import Monad.Instance.K.PreElgot
```