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

Progress on commutativity

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-13 16:24:28 +01:00
parent fb0d6f2799
commit c11ad1998c
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 132 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -21,6 +21,8 @@ open import Monad.Instance.K.Strong ambient MK
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.Compositionality ambient MK
open Equiv
open HomReasoning
@ -37,9 +39,11 @@ The proof is analogous to the ones for strength, the relevant diagram is:
```agda
open monadK using (μ)
open StrongMonad KStrong using (strengthen)
open kleisliK using (extend)
open strongK using (strengthen)
open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique; ♯ˡ-unique; ♯ˡ-preserving; ♯ˡ-law)
open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
#-Compositionality = λ {A X Y : Obj} {f : X ⇒ K.₀ A + X} {h : Y ⇒ X + Y} → Elgot-Algebra-on.#-Compositionality (elgot A) {X} {Y} {f} {h}
-- some helper definitions to make our life easier
private
@ -51,6 +55,38 @@ private
σ : ∀ ((X , Y) : Obj ×f Obj) → K.₀ X × Y ⇒ K.₀ (X × Y)
σ _ = K.₁ swap ∘ (τ _) ∘ swap
σ-η : ∀ {X Y} → σ (X , Y) ∘ (η _ ⁂ idC) ≈ η _
σ-η = begin
σ (_ , _) ∘ (η _ ⁂ idC) ≈⟨ pullʳ (pullʳ swap∘⁂) ⟩
K.₁ swap ∘ τ (_ , _) ∘ (idC ⁂ η _) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (τ-η _)) ⟩
K.₁ swap ∘ η _ ∘ swap ≈⟨ pullˡ (K₁η swap) ⟩
(η _ ∘ swap) ∘ swap ≈⟨ cancelʳ swap∘swap ⟩
η (_ × _) ∎
σ-comm : ∀ {X Y Z} (h : Z ⇒ K.₀ X + Z) → σ (X , Y) ∘ (h # ⁂ idC) ≈ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))#
σ-comm {X} {Y} {Z} h = begin
(K.₁ swap ∘ τ _ ∘ swap) ∘ (h # ⁂ idC) ≈⟨ pullʳ (pullʳ swap∘⁂) ⟩
K.₁ swap ∘ τ _ ∘ (idC ⁂ h #) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (τ-comm h)) ⟩
K.₁ swap ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ swap ≈⟨ pullˡ (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ swap))) ⟩
((K.₁ swap +₁ idC) ∘ (τ (Y , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ swap ≈⟨ sym (#-Uniformity (algebras _) (sym by-uni)) ⟩
((σ (X , Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∎
where
by-uni : ((K.₁ swap +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ≈ (idC +₁ swap) ∘ (σ (X , Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)
by-uni = begin
((K.₁ swap +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ≈⟨ pullʳ (pullʳ (pullʳ (sym swap∘⁂))) ⟩
(K.₁ swap +₁ idC) ∘ (τ (Y , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ swap ∘ (h ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ distributeˡ⁻¹∘swap ⟩
(K.₁ swap +₁ idC) ∘ (τ (Y , X) +₁ idC) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ⟩
(K.₁ swap ∘ τ _ +₁ idC ∘ idC) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc (elimˡ identity²))) ⟩
((σ _ +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ○ sym-assoc ⟩
(idC +₁ swap) ∘ (σ (X , Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ∎
extend-preserve : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (h : Z ⇒ K.₀ X + Z) → extend f ∘ h # ≈ ((extend f +₁ idC) ∘ h) #
extend-preserve {X} {Y} {Z} f h = begin
(μ.η _ ∘ K.₁ f) ∘ h # ≈⟨ pullʳ (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ f))) ⟩
μ.η _ ∘ ((K.₁ f +₁ idC) ∘ h) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩
((μ.η _ +₁ idC) ∘ (K.₁ f +₁ idC) ∘ h) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
((extend f +₁ idC) ∘ h) # ∎
proof-principle : ∀ {X Y} (f g : K.₀ X × K.₀ Y ⇒ K.₀ (X × Y)) → f ∘ (η _ ⁂ η _) ≈ g ∘ (η _ ⁂ η _) → (∀ {A} (h : A ⇒ K.₀ Y + A) → f ∘ (idC ⁂ h #) ≈ ((f +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#) → (∀ {A} (h : A ⇒ K.₀ X + A) → f ∘ (h # ⁂ idC) ≈ ((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) → (∀ {A} (h : A ⇒ K.₀ Y + A) → g ∘ (idC ⁂ h #) ≈ ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#) → (∀ {A} (h : A ⇒ K.₀ X + A) → g ∘ (h # ⁂ idC) ≈ ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) → f ≈ g
proof-principle {X} {Y} f g η-eq f-iter₁ f-iter₂ g-iter₁ g-iter₂ = begin
f ≈⟨ ♯-unique (stable _) (f ∘ (idC ⁂ η Y)) f refl (λ h → f-iter₁ h) ⟩
@ -91,7 +127,6 @@ KCommutative = record { commutes = commutes' }
commutes' {X} {Y} = begin
μ.η _ ∘ K.₁ (σ _) ∘ τ _ ≈⟨ ♯-unique (stable _) (σ _) (μ.η (X × Y) ∘ K.₁ (σ _) ∘ τ _) comm₁ comm₂ ⟩
(σ _) ♯ ≈⟨ sym (♯-unique (stable _) (σ _) (μ.η _ ∘ K.₁ (τ _) ∘ σ _) comm₃ comm₄) ⟩
{! !} ≈⟨ {! !} ⟩
μ.η _ ∘ K.₁ (τ _) ∘ σ _ ∎
where
comm₁ : σ _ ≈ (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _)
@ -124,21 +159,73 @@ KCommutative = record { commutes = commutes' }
σ _ ∎)
comm₄ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
comm₄ {Z} h = begin
(μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈⟨ {! !} ⟩
(μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ ⟨ ((π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # , ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ⟩ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
(μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈⟨ sym-assoc ⟩∘⟨refl ⟩
ψ ∘ (idC ⁂ h #) ≈⟨ ♯ˡ-unique (stable _) (τ (X , Y) ∘ (idC ⁂ (h #))) (ψ ∘ (idC ⁂ (h #))) (sym comm₅) comm₇ ⟩
(τ _ ∘ (idC ⁂ h #)) ♯ˡ ≈⟨ sym (♯ˡ-unique (stable _) (τ (X , Y) ∘ (idC ⁂ (h #))) (((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) (sym comm₆) comm₈) ⟩
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc refl) ⟩∘⟨refl) ⟩
((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
where
π₁-iter : ((π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈ π₁ ∘ (idC ⁂ h #)
π₁-iter = {! !}
distrib : (π₁ +₁ idC) ∘ distributeˡ⁻¹ ≈ i₁ ∘ π₁
distrib = Iso⇒Epi C (IsIso.iso isIsoˡ) ((π₁ +₁ idC) ∘ distributeˡ⁻¹) (i₁ ∘ π₁) (begin
((π₁ +₁ idC) ∘ distributeˡ⁻¹) ∘ distributeˡ ≈⟨ cancelʳ {! !} ⟩
(π₁ +₁ idC) ≈⟨ {! !} ⟩
ψ : ∀ {X Y} → K.₀ X × K.₀ Y ⇒ K.₀ (X × Y)
ψ = extend (τ _) ∘ σ _
comm₅ : (ψ ∘ (idC ⁂ (h #))) ∘ (η _ ⁂ idC) ≈ τ _ ∘ (idC ⁂ h #)
comm₅ = begin
(ψ ∘ (idC ⁂ (h #))) ∘ (η _ ⁂ idC) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm) ⟩
ψ ∘ (η _ ∘ idC ⁂ idC ∘ h #) ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩
ψ ∘ (η X ⁂ idC) ∘ (idC ⁂ (h #)) ≈⟨ pullˡ (pullʳ σ-η ) ⟩
(extend (τ _) ∘ η _) ∘ (idC ⁂ h #) ≈⟨ kleisliK.identityʳ ⟩∘⟨refl ⟩
τ (X , Y) ∘ (idC ⁂ (h #)) ∎
comm₆ : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (η _ ⁂ idC) ≈ τ _ ∘ (idC ⁂ h #)
comm₆ = begin
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ (η _ ⁂ idC) ≈⟨ sym (#-Uniformity (algebras _) (sym by-uni)) ⟩
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ sym (τ-comm h) ⟩
τ (X , Y) ∘ (idC ⁂ (h #)) ∎
where
by-uni : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ (η _ ⁂ idC) ≈ (idC +₁ (η _ ⁂ idC)) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
by-uni = begin
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ (η _ ⁂ idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm ○ sym ⁂∘⁂)) ⟩
(ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (η _ ⁂ idC) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ pullˡ (sym (distribute₁ _ _ _ ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym))) ⟩
(ψ +₁ idC) ∘ ((η _ ⁂ idC +₁ η _ ⁂ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ pullˡ (pullˡ +₁∘+₁) ⟩
((ψ ∘ (η _ ⁂ idC) +₁ idC ∘ (η _ ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ assoc ○ (+₁-cong₂ (pullʳ σ-η) identityˡ) ⟩∘⟨refl ⟩
(extend (τ _) ∘ η _ +₁ η _ ⁂ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ kleisliK.identityʳ refl) ⟩∘⟨refl ⟩
(τ _ +₁ (η _ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ sym (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) ⟩
(idC +₁ (η _ ⁂ idC)) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ∎
comm₇ : ∀ {U} (g : U ⇒ K.₀ X + U) → (ψ ∘ (idC ⁂ h #)) ∘ (g # ⁂ idC) ≈ ((ψ ∘ (idC ⁂ h #) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #
comm₇ {U} g = begin
(ψ ∘ (idC ⁂ h #)) ∘ (g # ⁂ idC) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm ○ sym ⁂∘⁂) ⟩
ψ ∘ (g # ⁂ idC) ∘ (idC ⁂ h #) ≈⟨ pullˡ (pullʳ (σ-comm g)) ⟩
(extend (τ _) ∘ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ (idC ⁂ h #) ≈⟨ extend-preserve (τ (X , Y)) _ ⟩∘⟨refl ⟩
((extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # ∘ (idC ⁂ h #) ≈⟨ sym (#-Uniformity (algebras _) (sym by-uni)) ⟩
((ψ ∘ (idC ⁂ h #) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
where
by-uni : ((extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) ∘ (idC ⁂ h #) ≈ (idC +₁ (idC ⁂ h #)) ∘ ((ψ ∘ (idC ⁂ h #)) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)
by-uni = begin
((extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm id-comm-sym ○ sym ⁂∘⁂))) ⟩
(extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (idC ⁂ (h #)) ∘ (g ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (distribute₁' _ _ _ ○ refl⟩∘⟨ ⁂-cong₂ ([]-unique id-comm-sym id-comm-sym) refl)) ⟩
(extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ ((idC ⁂ h # +₁ idC ⁂ h #) ∘ distributeʳ⁻¹) ∘ (g ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ○ pullˡ (pullˡ +₁∘+₁) ⟩
((ψ ∘ (idC ⁂ h #) +₁ (idC ∘ idC) ∘ (idC ⁂ h #)) ∘ distributeʳ⁻¹) ∘ (g ⁂ idC) ≈⟨ assoc ○ (+₁-cong₂ refl (elimˡ identity²)) ⟩∘⟨refl ⟩
(ψ ∘ (idC ⁂ h #) +₁ (idC ⁂ h #)) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩
(idC +₁ (idC ⁂ h #)) ∘ ((ψ ∘ (idC ⁂ h #)) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ∎
comm₈ : ∀ {U} (g : U ⇒ K.₀ X + U) → ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ (g # ⁂ idC) ≈ ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#
comm₈ {U} g = begin
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ {!!} ⟩ -- Uniformity
((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-Compositionality ⟩
( [ (idC +₁ i₁) ∘ (ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ [ i₁ , distributeˡ⁻¹ ∘ (idC ⁂ h) ]) # ∘ i₂ ≈⟨ {!!} ⟩
([ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ [ i₁ , distributeˡ⁻¹ ∘ (idC ⁂ h) ]) # ∘ i₂ ≈⟨ {!!} ⟩
[ [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ i₁ , [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ] # ∘ i₂ ≈⟨ {!!} ⟩
[ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ] # ∘ i₂ ≈⟨ {!!} ⟩
([ (ψ +₁ i₁) ∘ distributeʳ⁻¹ , [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ distributeˡ⁻¹ ] ∘ (g ⁂ idC +₁ idC ⁂ h)) # ∘ i₂ ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
i₁ ∘ [ π₁ , π₁ ] ≈˘⟨ {! !} ⟩
[ i₁ ∘ π₁ , i₁ ∘ π₁ ] ≈˘⟨ {! !} ⟩
[ i₁ ∘ idC ∘ π₁ , i₁ ∘ idC ∘ π₁ ] ≈˘⟨ []-cong₂ (pullʳ π₁∘⁂) (pullʳ π₁∘⁂) ⟩
[ (i₁ ∘ π₁) ∘ (idC ⁂ i₁) , (i₁ ∘ π₁) ∘ (idC ⁂ i₂) ] ≈˘⟨ ∘[] ⟩
(i₁ ∘ π₁) ∘ distributeˡ ∎)
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
([((ψ +₁ i₁) ∘ distributeʳ⁻¹) , (i₂ ∘ i₂ ∘ distributeʳ⁻¹) ] ∘ distributeˡ⁻¹ ∘ {!!}) # ∘ i₂ ∘ i₂ ≈⟨ {!!} ⟩
{!!} ≈˘⟨ {!!} ⟩
{!!} ≈˘⟨ {!!} ⟩
{!!} ≈˘⟨ {!!} ⟩
{!!} ≈˘⟨ {!!} ⟩
([ (idC +₁ i₁) ∘ (ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) , i₂ ∘ i₂ ] ∘ [ i₁ , distributeʳ⁻¹ ∘ (g ⁂ idC) ]) # ∘ i₂ ≈˘⟨ #-Compositionality ⟩
((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
```

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

@ -1,5 +1,30 @@
# TODO: every KX satisfies compositionality
```agda
module Monad.Instance.K.Compositionality where
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Categories.FreeObjects.Free
open import Category.Instance.AmbientCategory
import Monad.Instance.K as MIK
```
```agda
module Monad.Instance.K.Compositionality {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
open Ambient ambient
open MIK ambient
open MonadK MK
open import Algebra.UniformIterationAlgebra ambient
open import Algebra.ElgotAlgebra ambient
elgot : ∀ (A : Obj) → Elgot-Algebra-on (K.₀ A)
elgot A = record
{ _# = _#
; #-Fixpoint = #-Fixpoint
; #-Uniformity = #-Uniformity
; #-Folding = {! !}
; #-resp-≈ = #-resp-≈
}
where
open Uniform-Iteration-Algebra (algebras A) using (_#; #-Fixpoint; #-Uniformity; #-resp-≈)
```