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

update index

Browse source
This commit is contained in:
Leon Vatthauer 2024-02-14 12:03:47 +01:00
parent 041a4c1748
commit 896dc3d296
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
agda/src/index.lagda.md
View file

@ -57,6 +57,13 @@ Afterwards we also introduce categories of iteration algebras with iteration pre
open import Category.Construction.ElgotAlgebras
```
we can form products and exponentials in a canonical way:
```agda
open import Category.Construction.ElgotAlgebras.Products
open import Category.Construction.ElgotAlgebras.Exponentials
```
Free Elgot algebras are free objects in the category of Elgot algebras, we will be needing a notion of stability for them:
```agda
@ -67,7 +74,7 @@ open import Algebra.Elgot.Stable
In a CCC stability follows directly
```agda
open import Algebra.Elgot.Properties
```
```
With this in hand we can now define *KX* as a *free Elgot algebra* and proof that under *stability* it is a strong monad.
@ -83,7 +90,7 @@ 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 the initial (strong) pre-Elgot monad.
and lastly we formalize the notion of *(strong) pre-Elgot monad* and show that **K** is the initial (strong) pre-Elgot monad.
```agda
open import Monad.PreElgot