diff --git a/src/Monad/Instance/K/Commutative.lagda.md b/src/Monad/Instance/K/Commutative.lagda.md index 1a0189f..751334f 100644 --- a/src/Monad/Instance/K/Commutative.lagda.md +++ b/src/Monad/Instance/K/Commutative.lagda.md @@ -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) ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - i₁ ∘ [ π₁ , π₁ ] ≈˘⟨ {! !} ⟩ - [ i₁ ∘ π₁ , i₁ ∘ π₁ ] ≈˘⟨ {! !} ⟩ - [ i₁ ∘ idC ∘ π₁ , i₁ ∘ idC ∘ π₁ ] ≈˘⟨ []-cong₂ (pullʳ π₁∘⁂) (pullʳ π₁∘⁂) ⟩ - [ (i₁ ∘ π₁) ∘ (idC ⁂ i₁) , (i₁ ∘ π₁) ∘ (idC ⁂ i₂) ] ≈˘⟨ ∘[] ⟩ - (i₁ ∘ π₁) ∘ distributeˡ ∎) -``` \ No newline at end of file + ψ : ∀ {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₁) ∘ 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))# ∎ + +``` diff --git a/src/Monad/Instance/K/Compositionality.lagda.md b/src/Monad/Instance/K/Compositionality.lagda.md index 771a00b..ee365cc 100644 --- a/src/Monad/Instance/K/Compositionality.lagda.md +++ b/src/Monad/Instance/K/Compositionality.lagda.md @@ -1,5 +1,30 @@ # TODO: every KX satisfies compositionality ```agda -module Monad.Instance.K.Compositionality where -``` \ No newline at end of file +{-# 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-≈) +```