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

Proof that KX is freeElgot (still assuming compositionality)

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-15 09:41:27 +01:00
parent 13450c1d23
commit a877cd3f25
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 20 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Monad/Instance/K/Compositionality.lagda.md
View file

@ -15,7 +15,12 @@ module Monad.Instance.K.Compositionality {o ℓ e} (ambient : Ambient o ℓ e) (
open MonadK MK open MonadK MK
open import Algebra.UniformIterationAlgebra ambient open import Algebra.UniformIterationAlgebra ambient
open import Category.Construction.UniformIterationAlgebras ambient
open import Category.Construction.ElgotAlgebras ambient
open import Algebra.ElgotAlgebra ambient open import Algebra.ElgotAlgebra ambient
open import Algebra.Properties ambient
open import Categories.Functor.Core
open Functor using (F₀; F₁)
elgot : ∀ (A : Obj) → Elgot-Algebra-on (K.₀ A) elgot : ∀ (A : Obj) → Elgot-Algebra-on (K.₀ A)
elgot A = record elgot A = record
@ -27,4 +32,19 @@ module Monad.Instance.K.Compositionality {o ℓ e} (ambient : Ambient o ℓ e) (
} }
where where
open Uniform-Iteration-Algebra (algebras A) using (_#; #-Fixpoint; #-Uniformity; #-resp-≈) open Uniform-Iteration-Algebra (algebras A) using (_#; #-Fixpoint; #-Uniformity; #-resp-≈)
freeElgot : ∀ (A : Obj) → FreeElgotAlgebra A
freeElgot A = record
{ FX = record { A = K.₀ A ; algebra = elgot A }
; η = η (freealgebras A)
; _* = λ {X} f → record
{ h = Uniform-Iteration-Algebra-Morphism.h (_* (freealgebras A) {A = F₀ elgot-to-uniformF X} f)
; preserves = λ {Y} {g} → Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras A) *) f)
}
; *-lift = *-lift (freealgebras A)
; *-uniq = λ {X} f g eq → *-uniq (freealgebras A) f (F₁ elgot-to-uniformF g) eq
}
where
open FreeObject using (η; _*; *-lift; *-uniq)
``` ```
2