From 161ceabcdaa68ef00e604debee7126b5cf2b3aa4 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 5 Feb 2024 18:12:58 +0100 Subject: [PATCH] Finish proof that D~~ is instance of K on setoids. Did some refactor on StableFreeElgotAlgebras, proved that left-stable and right-stable imply each other --- agda/src/Algebra/Elgot/Properties.lagda.md | 31 +-- agda/src/Algebra/Elgot/Stable.lagda.md | 175 ++++++++++----- .../Construction/ElgotAlgebras.lagda.md | 209 +++++++++--------- .../src/Monad/Instance/K/Commutative.lagda.md | 14 +- agda/src/Monad/Instance/Setoids/K.lagda.md | 8 +- 5 files changed, 254 insertions(+), 183 deletions(-) diff --git a/agda/src/Algebra/Elgot/Properties.lagda.md b/agda/src/Algebra/Elgot/Properties.lagda.md index 1807b89..b076444 100644 --- a/agda/src/Algebra/Elgot/Properties.lagda.md +++ b/agda/src/Algebra/Elgot/Properties.lagda.md @@ -33,8 +33,9 @@ module Algebra.Elgot.Properties {o ℓ e} {C : Category o ℓ e} (distributive : open Cartesian cartesian open BinaryProducts products hiding (η) renaming (unique to ⟨⟩-unique) open Cocartesian cocartesian - ccc : CartesianClosed C - ccc = record { cartesian = cartesian ; exp = expos } + private + ccc : CartesianClosed C + ccc = record { cartesian = cartesian ; exp = expos } open CartesianClosed ccc hiding (exp; cartesian) @@ -45,20 +46,18 @@ module Algebra.Elgot.Properties {o ℓ e} {C : Category o ℓ e} (distributive : open import Algebra.Elgot.Free cocartesian open import Algebra.Elgot.Stable distributive - open CartesianClosed Elgot-CCC using () renaming (λg to λg#; _^_ to _^#_) - open Elgot-Algebra-Morphism renaming (h to <_>) - stable : ∀ {Y} (fe : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebraˡ fe - IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (stable {Y} fe) {X} A f = (eval′ ∘ (< FreeObject._* fe {B^A-Helper {A} {X}} (λg f) > ⁂ id)) + free-isStableˡ : ∀ {Y} (fe : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebraˡ fe + IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (free-isStableˡ {Y} fe) {X} A f = (eval′ ∘ (< FreeObject._* fe {B^A-Helper {A} {X}} (λg f) > ⁂ id)) where open FreeObject fe - IsStableFreeElgotAlgebraˡ.♯ˡ-law (stable {Y} fe) {X} {A} f = sym (begin + IsStableFreeElgotAlgebraˡ.♯ˡ-law (free-isStableˡ {Y} fe) {X} {A} f = sym (begin (eval′ ∘ (< (λg f)* > ⁂ id)) ∘ (η ⁂ id) ≈⟨ pullʳ ⁂∘⁂ ⟩ eval′ ∘ ((< (λg f)* > ∘ η) ⁂ id ∘ id) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (*-lift (λg f)) identity²) ⟩ eval′ ∘ (λg f ⁂ id) ≈⟨ β′ ⟩ f ∎) where open FreeObject fe - IsStableFreeElgotAlgebraˡ.♯ˡ-preserving (stable {Y} fe) {X} {B} f {Z} h = begin + IsStableFreeElgotAlgebraˡ.♯ˡ-preserving (free-isStableˡ {Y} fe) {X} {B} f {Z} h = begin (eval′ ∘ (< (λg f)* > ⁂ id)) ∘ (h #ʸ ⁂ id) ≈⟨ pullʳ ⁂∘⁂ ⟩ eval′ ∘ (< (λg f)* > ∘ h #ʸ ⁂ id ∘ id) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (preserves ((λg f)*)) identity²) ⟩ eval′ ∘ (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((< (λg f)* > +₁ id) ∘ h ⁂ id)) #ᵇ) ⁂ id) ≈⟨ β′ ⟩ @@ -70,12 +69,16 @@ module Algebra.Elgot.Properties {o ℓ e} {C : Category o ℓ e} (distributive : open FreeObject fe renaming (FX to KY) open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-resp-≈ to #ᵇ-resp-≈) open Elgot-Algebra KY using () renaming (_# to _#ʸ) - IsStableFreeElgotAlgebraˡ.♯ˡ-unique (stable {Y} fe) {X} {B} f g eq₁ eq₂ = sym (begin - eval′ ∘ (< (λg f)* > ⁂ id) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (*-cong (λ-cong eq₁)) refl) ⟩ - eval′ ∘ (< (λg (g ∘ (η ⁂ id)))* > ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂-cong₂ (*-cong subst) refl) ⟩ - eval′ ∘ (< (λg g ∘ η)* > ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂-cong₂ (*-uniq (λg g ∘ η) (record { h = λg g ; preserves = {! !} }) refl) refl) ⟩ - eval′ ∘ (λg g ⁂ id) ≈⟨ β′ ⟩ - g ∎) + IsStableFreeElgotAlgebraˡ.♯ˡ-unique (free-isStableˡ {Y} fe) {X} {B} f g eq₁ eq₂ = λ-inj (begin + λg g ≈⟨ *-uniq (λg f) (record { h = λg g ; preserves = λ {D} {h} → begin + λg g ∘ (h #ʸ) ≈⟨ subst ⟩ + λg (g ∘ (h #ʸ ⁂ id)) ≈⟨ λ-cong (eq₂ h) ⟩ + λg (((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ) ≈˘⟨ λ-cong (#ᵇ-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ (elimʳ (⟨⟩-unique id-comm id-comm))))) ⟩ + λg (((eval′ +₁ id) ∘ (λg g ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ) ≈˘⟨ λ-cong (#ᵇ-resp-≈ (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (λg g) id)) ○ assoc))) ⟩ + λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg g +₁ id) ⁂ id) ∘ (h ⁂ id)) #ᵇ) ≈⟨ λ-cong (#ᵇ-resp-≈ (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩ + λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg g +₁ id) ∘ h ⁂ id)) #ᵇ) ∎ }) (subst ○ λ-cong (sym eq₁)) ⟩ + < (λg f)* > ≈˘⟨ η-exp′ ⟩ + λg (eval′ ∘ (< (λg f)* > ⁂ id)) ∎) where open FreeObject fe renaming (FX to KY) open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-resp-≈ to #ᵇ-resp-≈) diff --git a/agda/src/Algebra/Elgot/Stable.lagda.md b/agda/src/Algebra/Elgot/Stable.lagda.md index efcb583..f7652db 100644 --- a/agda/src/Algebra/Elgot/Stable.lagda.md +++ b/agda/src/Algebra/Elgot/Stable.lagda.md @@ -61,7 +61,6 @@ Stable free Elgot algebras have an additional universal iteration preserving mor open Elgot-Algebra FY using (_#) field - -- TODO awkward notation... [_,_]♯ : ∀ {X : Obj} (A : Elgot-Algebra) (f : X × Y ⇒ Elgot-Algebra.A A) → X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A A ♯-law : ∀ {X : Obj} {A : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A A) → f ≈ [ A , f ]♯ ∘ (id ⁂ η) ♯-preserving : ∀ {X : Obj} {B : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → [ B , f ]♯ ∘ (id ⁂ h #) ≈ Elgot-Algebra._# B (([ B , f ]♯ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) @@ -69,58 +68,124 @@ Stable free Elgot algebras have an additional universal iteration preserving mor → f ≈ g ∘ (id ⁂ η) → (∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (id ⁂ h #) ≈ Elgot-Algebra._# B ((g +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))) → g ≈ [ B , f ]♯ - [_,_]♯ˡ : ∀ {X : Obj} (A : Elgot-Algebra) (f : Y × X ⇒ Elgot-Algebra.A A) → Elgot-Algebra.A FY × X ⇒ Elgot-Algebra.A A - [_,_]♯ˡ {X} A f = [ A , (f ∘ swap) ]♯ ∘ swap - ♯ˡ-law : ∀ {X : Obj} {A : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A A) → f ≈ [ A , f ]♯ˡ ∘ (η ⁂ id) - ♯ˡ-law {X} {A} f = begin - f ≈⟨ introʳ swap∘swap ⟩ - f ∘ swap ∘ swap ≈⟨ pullˡ (♯-law (f ∘ swap)) ⟩ - ([ A , f ∘ swap ]♯ ∘ (id ⁂ η)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩ - [ A , (f ∘ swap) ]♯ ∘ swap ∘ (η ⁂ id) ≈⟨ sym-assoc ⟩ - ([ A , (f ∘ swap) ]♯ ∘ swap) ∘ (η ⁂ id) ∎ - ♯ˡ-preserving : ∀ {X : Obj} {B : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → [ B , f ]♯ˡ ∘ (h # ⁂ id) ≈ Elgot-Algebra._# B (([ B , f ]♯ˡ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) - ♯ˡ-preserving {X} {B} f {Z} h = begin - ([ B , (f ∘ swap) ]♯ ∘ swap) ∘ ((h #) ⁂ id) ≈⟨ pullʳ swap∘⁂ ⟩ - [ B , (f ∘ swap) ]♯ ∘ (id ⁂ h #) ∘ swap ≈⟨ pullˡ (♯-preserving (f ∘ swap) h) ⟩ - (([ B , (f ∘ swap) ]♯ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩ - ((([ B , (f ∘ swap) ]♯ ∘ swap) +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∎ - where - open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) - uni-helper : (id +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈ (([ B , f ∘ swap ]♯ coproducts.+₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) ∘ swap - uni-helper = begin - (id +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ pullˡ +₁∘+₁ ⟩ - (id ∘ [ B , f ∘ swap ]♯ ∘ swap +₁ swap ∘ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ - ([ B , f ∘ swap ]♯ ∘ swap +₁ id ∘ swap) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ - (([ B , f ∘ swap ]♯ +₁ id) ∘ (swap +₁ swap)) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹∘swap)) ⟩ - ([ B , f ∘ swap ]♯ +₁ id) ∘ (distributeˡ⁻¹ ∘ swap) ∘ (h ⁂ id) ≈⟨ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc ⟩ - (([ B , f ∘ swap ]♯ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) ∘ swap ∎ - ♯ˡ-unique : ∀ {X : Obj} {B : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A B) (g : Elgot-Algebra.A FY × X ⇒ Elgot-Algebra.A B) - → f ≈ g ∘ (η ⁂ id) - → ({Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (h # ⁂ id) ≈ Elgot-Algebra._# B ((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id))) - → g ≈ [ B , f ]♯ˡ - ♯ˡ-unique {X} {B} f g g-law g-preserving = begin - g ≈⟨ introʳ swap∘swap ⟩ - g ∘ swap ∘ swap ≈⟨ sym-assoc ⟩ - (g ∘ swap) ∘ swap ≈⟨ (♯-unique (f ∘ swap) (g ∘ swap) helper₁ helper₂) ⟩∘⟨refl ⟩ - [ B , (f ∘ swap) ]♯ ∘ swap ∎ - where - open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) - helper₁ : f ∘ swap ≈ (g ∘ swap) ∘ (id ⁂ η) - helper₁ = begin - f ∘ swap ≈⟨ g-law ⟩∘⟨refl ⟩ - (g ∘ (η ⁂ id)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩ - g ∘ swap ∘ (id ⁂ η) ≈⟨ sym-assoc ⟩ - (g ∘ swap) ∘ (id ⁂ η) ∎ - helper₂ : ∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → (g ∘ swap) ∘ (id ⁂ h #) ≈ ((g ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ - helper₂ {Z} h = begin - (g ∘ swap) ∘ (id ⁂ h #) ≈⟨ pullʳ swap∘⁂ ⟩ - g ∘ (h # ⁂ id) ∘ swap ≈⟨ pullˡ (g-preserving h) ⟩ - ((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩ - ((g ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ ∎ - where - uni-helper : (id +₁ swap) ∘ (g ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈ ((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ∘ swap - uni-helper = pullˡ +₁∘+₁ ○ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ○ (sym +₁∘+₁) ⟩∘⟨refl ○ pullʳ (pullˡ (sym distributeʳ⁻¹∘swap)) ○ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc + isStable⇒isStableˡ : ∀ {Y} (freeElgot : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebra {Y} freeElgot → IsStableFreeElgotAlgebraˡ {Y} freeElgot + + IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (isStable⇒isStableˡ {Y} fe isStable) {X} A f = [ A , (f ∘ swap) ]♯ ∘ swap + where open IsStableFreeElgotAlgebra isStable + + IsStableFreeElgotAlgebraˡ.♯ˡ-law (isStable⇒isStableˡ {Y} fe isStable) {X} {A} f = begin + f ≈⟨ introʳ swap∘swap ⟩ + f ∘ swap ∘ swap ≈⟨ pullˡ (♯-law (f ∘ swap)) ⟩ + ([ A , f ∘ swap ]♯ ∘ (id ⁂ η)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩ + [ A , (f ∘ swap) ]♯ ∘ swap ∘ (η ⁂ id) ≈⟨ sym-assoc ⟩ + ([ A , (f ∘ swap) ]♯ ∘ swap) ∘ (η ⁂ id) ∎ + where + open IsStableFreeElgotAlgebra isStable + open FreeObject fe using (η) renaming (FX to FY) + + IsStableFreeElgotAlgebraˡ.♯ˡ-preserving (isStable⇒isStableˡ {Y} fe isStable) {X} {B} f {Z} h = begin + ([ B , (f ∘ swap) ]♯ ∘ swap) ∘ ((h #) ⁂ id) ≈⟨ pullʳ swap∘⁂ ⟩ + [ B , (f ∘ swap) ]♯ ∘ (id ⁂ h #) ∘ swap ≈⟨ pullˡ (♯-preserving (f ∘ swap) h) ⟩ + (([ B , (f ∘ swap) ]♯ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩ + ((([ B , (f ∘ swap) ]♯ ∘ swap) +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∎ + where + open IsStableFreeElgotAlgebra isStable + open FreeObject fe using (η) renaming (FX to FY) + open Elgot-Algebra FY using (_#) + open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) + uni-helper : (id +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈ (([ B , f ∘ swap ]♯ coproducts.+₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) ∘ swap + uni-helper = begin + (id +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ pullˡ +₁∘+₁ ⟩ + (id ∘ [ B , f ∘ swap ]♯ ∘ swap +₁ swap ∘ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ + ([ B , f ∘ swap ]♯ ∘ swap +₁ id ∘ swap) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ + (([ B , f ∘ swap ]♯ +₁ id) ∘ (swap +₁ swap)) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹∘swap)) ⟩ + ([ B , f ∘ swap ]♯ +₁ id) ∘ (distributeˡ⁻¹ ∘ swap) ∘ (h ⁂ id) ≈⟨ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc ⟩ + (([ B , f ∘ swap ]♯ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) ∘ swap ∎ + + IsStableFreeElgotAlgebraˡ.♯ˡ-unique (isStable⇒isStableˡ {Y} fe isStable) {X} {B} f g g-law g-preserving = begin + g ≈⟨ introʳ swap∘swap ⟩ + g ∘ swap ∘ swap ≈⟨ pullˡ (♯-unique (f ∘ swap) (g ∘ swap) helper₁ helper₂) ⟩ + [ B , (f ∘ swap) ]♯ ∘ swap ∎ + where + open IsStableFreeElgotAlgebra isStable + open FreeObject fe using (η) renaming (FX to FY) + open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) + open Elgot-Algebra FY using (_#) + helper₁ : f ∘ swap ≈ (g ∘ swap) ∘ (id ⁂ η) + helper₁ = begin + f ∘ swap ≈⟨ g-law ⟩∘⟨refl ⟩ + (g ∘ (η ⁂ id)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩ + g ∘ swap ∘ (id ⁂ η) ≈⟨ sym-assoc ⟩ + (g ∘ swap) ∘ (id ⁂ η) ∎ + helper₂ : ∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → (g ∘ swap) ∘ (id ⁂ h #) ≈ ((g ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ + helper₂ {Z} h = begin + (g ∘ swap) ∘ (id ⁂ h #) ≈⟨ pullʳ swap∘⁂ ⟩ + g ∘ (h # ⁂ id) ∘ swap ≈⟨ pullˡ (g-preserving h) ⟩ + ((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩ + ((g ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ ∎ + where + uni-helper : (id +₁ swap) ∘ (g ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈ ((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ∘ swap + uni-helper = pullˡ +₁∘+₁ ○ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ○ (sym +₁∘+₁) ⟩∘⟨refl ○ pullʳ (pullˡ (sym distributeʳ⁻¹∘swap)) ○ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc + + isStableˡ⇒isStable : ∀ {Y} (freeElgot : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebraˡ {Y} freeElgot → IsStableFreeElgotAlgebra {Y} freeElgot + + IsStableFreeElgotAlgebra.[_,_]♯ (isStableˡ⇒isStable {Y} fe isStableˡ) {X} A f = [ A , f ∘ swap ]♯ˡ ∘ swap + where open IsStableFreeElgotAlgebraˡ isStableˡ + + IsStableFreeElgotAlgebra.♯-law (isStableˡ⇒isStable {Y} fe isStableˡ) {X} {A} f = begin + f ≈⟨ introʳ swap∘swap ⟩ + f ∘ swap ∘ swap ≈⟨ pullˡ (♯ˡ-law (f ∘ swap)) ⟩ + ([ A , f ∘ swap ]♯ˡ ∘ (η ⁂ id)) ∘ swap ≈⟨ (pullʳ (sym swap∘⁂)) ○ sym-assoc ⟩ + ([ A , (f ∘ swap) ]♯ˡ ∘ swap) ∘ (id ⁂ η) ∎ + where + open IsStableFreeElgotAlgebraˡ isStableˡ + open FreeObject fe using (η) renaming (FX to FY) + + IsStableFreeElgotAlgebra.♯-preserving (isStableˡ⇒isStable {Y} fe isStableˡ) {X} {B} f {Z} h = begin + ([ B , (f ∘ swap) ]♯ˡ ∘ swap) ∘ (id ⁂ h #) ≈⟨ pullʳ swap∘⁂ ⟩ + [ B , (f ∘ swap) ]♯ˡ ∘ ((h #) ⁂ id) ∘ swap ≈⟨ pullˡ (♯ˡ-preserving (f ∘ swap) h) ⟩ + (([ B , (f ∘ swap) ]♯ˡ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∘ swap ≈˘⟨ #ᵇ-Uniformity by-uni ⟩ + (((([ B , (f ∘ swap) ]♯ˡ ∘ swap) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ) ∎ + where + open IsStableFreeElgotAlgebraˡ isStableˡ + open FreeObject fe using (η) renaming (FX to FY) + open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) + open Elgot-Algebra FY using (_#) + by-uni : (id +₁ swap) ∘ ([ B , f ∘ swap ]♯ˡ ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈ (([ B , f ∘ swap ]♯ˡ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ∘ swap + by-uni = begin + (id +₁ swap) ∘ ([ B , f ∘ swap ]♯ˡ ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩ + (id ∘ [ B , f ∘ swap ]♯ˡ ∘ swap +₁ swap ∘ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ + ([ B , f ∘ swap ]♯ˡ ∘ swap +₁ id ∘ swap) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ + (([ B , f ∘ swap ]♯ˡ +₁ id) ∘ (swap +₁ swap)) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈⟨ pullʳ (pullˡ (sym distributeʳ⁻¹∘swap)) ⟩ + ([ B , f ∘ swap ]♯ˡ +₁ id) ∘ (distributeʳ⁻¹ ∘ swap) ∘ (id ⁂ h) ≈⟨ refl⟩∘⟨ (pullʳ swap∘⁂) ⟩ + ([ B , f ∘ swap ]♯ˡ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ∘ swap ≈˘⟨ assoc ○ refl⟩∘⟨ assoc ⟩ + (([ B , f ∘ swap ]♯ˡ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ∘ swap ∎ + + IsStableFreeElgotAlgebra.♯-unique (isStableˡ⇒isStable {Y} fe isStableˡ) {X} {B} f g g-law g-preserving = begin + g ≈⟨ introʳ swap∘swap ⟩ + g ∘ swap ∘ swap ≈⟨ pullˡ (♯ˡ-unique (f ∘ swap) (g ∘ swap) helper₁ helper₂) ⟩ + [ B , f ∘ swap ]♯ˡ ∘ swap ∎ + where + open IsStableFreeElgotAlgebraˡ isStableˡ + open FreeObject fe using (η) renaming (FX to FY) + open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) + open Elgot-Algebra FY using (_#) + helper₁ : f ∘ swap ≈ (g ∘ swap) ∘ (η ⁂ id) + helper₁ = begin + f ∘ swap ≈⟨ g-law ⟩∘⟨refl ⟩ + (g ∘ (id ⁂ η)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩ + g ∘ swap ∘ (η ⁂ id) ≈⟨ sym-assoc ⟩ + (g ∘ swap) ∘ (η ⁂ id) ∎ + helper₂ : ∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → (g ∘ swap) ∘ (h # ⁂ id) ≈ ((g ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ + helper₂ {Z} h = begin + (g ∘ swap) ∘ (h # ⁂ id) ≈⟨ pullʳ swap∘⁂ ⟩ + g ∘ (id ⁂ h #) ∘ swap ≈⟨ pullˡ (g-preserving h) ⟩ + ((g +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩ + ((g ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∎ + where + uni-helper : (id +₁ swap) ∘ (g ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈ ((g +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) ∘ swap + uni-helper = pullˡ +₁∘+₁ ○ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ○ (sym +₁∘+₁) ⟩∘⟨refl ○ pullʳ (pullˡ (sym distributeˡ⁻¹∘swap)) ○ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc record StableFreeElgotAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where field @@ -130,9 +195,3 @@ Stable free Elgot algebras have an additional universal iteration preserving mor open IsStableFreeElgotAlgebra isStableFreeElgotAlgebra public ``` - -In a cartesian closed category stability is derivable - -```agda - -- TODO -``` diff --git a/agda/src/Category/Construction/ElgotAlgebras.lagda.md b/agda/src/Category/Construction/ElgotAlgebras.lagda.md index 95fe405..cf4689a 100644 --- a/agda/src/Category/Construction/ElgotAlgebras.lagda.md +++ b/agda/src/Category/Construction/ElgotAlgebras.lagda.md @@ -316,113 +316,114 @@ module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} wher open Elgot-Algebra-Morphism renaming (h to <_>) - cccc : CanonicalCartesianClosed Elgot-Algebras - CanonicalCartesianClosed.⊤ cccc = Terminal.⊤ Terminal-Elgot-Algebras - CanonicalCartesianClosed._×_ cccc X Y = A×B-Helper {X} {Y} - CanonicalCartesianClosed.! cccc = Terminal.! Terminal-Elgot-Algebras - CanonicalCartesianClosed.π₁ cccc {X} {Y} = Product.π₁ (Product-Elgot-Algebras X Y) - CanonicalCartesianClosed.π₂ cccc {X} {Y} = Product.π₂ (Product-Elgot-Algebras X Y) - CanonicalCartesianClosed.⟨_,_⟩ cccc {X} {Y} {Z} f g = Product.⟨_,_⟩ (Product-Elgot-Algebras Y Z) f g - CanonicalCartesianClosed.!-unique cccc = Terminal.!-unique Terminal-Elgot-Algebras - CanonicalCartesianClosed.π₁-comp cccc {X} {Y} {f} {Z} {g} = Product.project₁ (Product-Elgot-Algebras Y Z) {h = f} {i = g} - CanonicalCartesianClosed.π₂-comp cccc {X} {Y} {f} {Z} {g} = Product.project₂ (Product-Elgot-Algebras Y Z) {h = f} {i = g} - CanonicalCartesianClosed.⟨,⟩-unique cccc {C} {A} {B} {f} {g} {h} eq₁ eq₂ = Product.unique (Product-Elgot-Algebras A B) {h = h} {i = f} {j = g} eq₁ eq₂ - CanonicalCartesianClosed._^_ cccc A X = B^A-Helper {A} {Elgot-Algebra.A X} - (Elgot-Algebra-Morphism.h) (CanonicalCartesianClosed.eval cccc {A} {B}) = eval′ - (Elgot-Algebra-Morphism.preserves) (CanonicalCartesianClosed.eval cccc {A} {B}) {X} {f} = begin - eval′ ∘ ⟨ (λg ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)))) , _ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ - eval′ ∘ ((λg ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)))) ⁂ id) ∘ ⟨ id , _ ⟩ ≈⟨ pullˡ β′ ⟩ - ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id))) ∘ ⟨ id , _ ⟩ ≈˘⟨ Elgot-Algebra.#-Uniformity A by-uni ⟩ - (Elgot-Algebra._# A) ((eval′ +₁ id) ∘ f) ∎ -- ⟨ ((π₁ +₁ id) ∘ h)#ᵃ , ((π₂ +₁ id) ∘ h)#ᵇ ⟩ - where - by-uni : (id +₁ ⟨ id , _ ⟩) ∘ ((eval′ +₁ id) ∘ f) ≈ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)) ∘ ⟨ id , _ ⟩ - by-uni = begin - (id +₁ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩) ∘ ((eval′ +₁ id) ∘ f) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ - (eval′ +₁ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩) ∘ f ≈˘⟨ sym-assoc ○ sym-assoc ○ (sym (+-unique by-inj₁ by-inj₂)) ⟩∘⟨refl ⟩ - (eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩ ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ refl assoc) ⟩ - (eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ ⟨ id ∘ f , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ∘ f ⟩ ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (⟨⟩-cong₂ refl (Elgot-Algebra.#-Fixpoint B))) ⟩ - (eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ ⟨ id ∘ f , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈˘⟨ pullʳ (pullʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ id-comm identityˡ)) ⟩ - ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈˘⟨ (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id π₁ id)))) ⟩∘⟨refl ⟩ - ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ⁂ id) ∘ (f ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩∘⟨refl ⟩ - ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎ - where - by-inj₁ : (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₁ ≈ i₁ ∘ eval′ - by-inj₁ = begin - (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₁ ≈⟨ pullʳ ⟨⟩∘ ⟩ - ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id ∘ i₁ , ([ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id)) ∘ i₁ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ id-comm-sym (pullʳ inject₁ ○ pullˡ inject₁ ○ identityˡ)) ⟩ - ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ i₁ ∘ id , π₂ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ refl identityˡ) ⟩ - ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ (i₁ ⁂ id) ∘ ⟨ id , π₂ ⟩ ≈⟨ pullʳ (pullʳ (pullˡ distributeʳ⁻¹-i₁)) ⟩ - (eval′ +₁ id) ∘ (π₁ ⁂ id +₁ id ⁂ id) ∘ i₁ ∘ ⟨ id , π₂ ⟩ ≈⟨ refl⟩∘⟨ (pullˡ +₁∘i₁) ⟩ - (eval′ +₁ id) ∘ (i₁ ∘ (π₁ ⁂ id)) ∘ ⟨ id , π₂ ⟩ ≈⟨ pullˡ (pullˡ +₁∘i₁) ⟩ - ((i₁ ∘ eval′) ∘ (π₁ ⁂ id)) ∘ ⟨ id , π₂ ⟩ ≈⟨ cancelʳ (⁂∘⟨⟩ ○ (⟨⟩-cong₂ identityʳ identityˡ) ○ ⟨⟩-unique identityʳ identityʳ) ⟩ - i₁ ∘ eval′ ∎ - by-inj₂ : (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₂ ≈ i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ - by-inj₂ = begin - (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₂ ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ id-comm-sym (pullʳ inject₂)) ⟩ - ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ i₂ ∘ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ i₂ ∘ id ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ identityʳ ○ inject₂)) ⟩ - ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ i₂ ∘ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ refl identityˡ) ⟩ - ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ (i₂ ⁂ id) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ pullʳ (pullʳ (pullˡ distributeʳ⁻¹-i₂)) ⟩ - (eval′ +₁ id) ∘ (π₁ ⁂ id +₁ id ⁂ id) ∘ i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ refl⟩∘⟨ (pullˡ inject₂) ⟩ - (eval′ +₁ id) ∘ (i₂ ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ pullˡ (pullˡ inject₂) ⟩ - ((i₂ ∘ id) ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ (cancelʳ (identityˡ ○ ⟨⟩-unique id-comm id-comm)) ⟩∘⟨refl ⟩ - i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎ - < CanonicalCartesianClosed.curry cccc {A} {B} {C} f > = λg < f > - preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = begin - λg < f > ∘ g #ᵃ ≈⟨ subst ⟩ - λg (< f > ∘ (g #ᵃ ⁂ id)) ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - λg (< f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩) ≈⟨ λ-cong (preserves f) ⟩ - λg (((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ) ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) #ᶜ) ∎ - where - open Elgot-Algebra A using () renaming (_# to _#ᵃ; #-Uniformity to #ᵃ-Uniformity) - open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) - open Elgot-Algebra C using () renaming (_# to _#ᶜ; #-resp-≈ to #ᶜ-resp-≈) - -- Elgot-Algebra-Morphism.preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = λ-unique′ (begin - -- eval′ ∘ ((λg < f > ∘ g #ᵃ) ⁂ id) ≈⟨ refl⟩∘⟨ ⁂-cong₂ subst refl ⟩ - -- eval′ ∘ ((λg (< f > ∘ (g #ᵃ ⁂ id))) ⁂ id) ≈⟨ β′ ⟩ - -- < f > ∘ (g #ᵃ ⁂ id) ≈⟨ refl⟩∘⟨ (⟨⟩-unique by-π₁ by-π₂) ⟩ - -- < f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈⟨ Elgot-Algebra-Morphism.preserves f ⟩ - -- ((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ ≈˘⟨ #ᶜ-resp-≈ (refl⟩∘⟨ assoc ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩ - -- ((eval′ +₁ id) ∘ (((λg < f > ⁂ id) +₁ (id ⁂ id)) ∘ distributeʳ⁻¹) ∘ (g ⁂ id)) #ᶜ ≈˘⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (λg < f >) id)))) ⟩ - -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg < f > +₁ id) ⁂ id) ∘ (g ⁂ id)) #ᶜ ≈⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩ - -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) #ᶜ ∎) + -- cccc : CanonicalCartesianClosed Elgot-Algebras + -- CanonicalCartesianClosed.⊤ cccc = Terminal.⊤ Terminal-Elgot-Algebras + -- CanonicalCartesianClosed._×_ cccc X Y = A×B-Helper {X} {Y} + -- CanonicalCartesianClosed.! cccc = Terminal.! Terminal-Elgot-Algebras + -- CanonicalCartesianClosed.π₁ cccc {X} {Y} = Product.π₁ (Product-Elgot-Algebras X Y) + -- CanonicalCartesianClosed.π₂ cccc {X} {Y} = Product.π₂ (Product-Elgot-Algebras X Y) + -- CanonicalCartesianClosed.⟨_,_⟩ cccc {X} {Y} {Z} f g = Product.⟨_,_⟩ (Product-Elgot-Algebras Y Z) f g + -- CanonicalCartesianClosed.!-unique cccc = Terminal.!-unique Terminal-Elgot-Algebras + -- CanonicalCartesianClosed.π₁-comp cccc {X} {Y} {f} {Z} {g} = Product.project₁ (Product-Elgot-Algebras Y Z) {h = f} {i = g} + -- CanonicalCartesianClosed.π₂-comp cccc {X} {Y} {f} {Z} {g} = Product.project₂ (Product-Elgot-Algebras Y Z) {h = f} {i = g} + -- CanonicalCartesianClosed.⟨,⟩-unique cccc {C} {A} {B} {f} {g} {h} eq₁ eq₂ = Product.unique (Product-Elgot-Algebras A B) {h = h} {i = f} {j = g} eq₁ eq₂ + -- CanonicalCartesianClosed._^_ cccc A X = B^A-Helper {A} {Elgot-Algebra.A X} + -- (Elgot-Algebra-Morphism.h) (CanonicalCartesianClosed.eval cccc {A} {B}) = eval′ + -- (Elgot-Algebra-Morphism.preserves) (CanonicalCartesianClosed.eval cccc {A} {B}) {X} {f} = begin + -- eval′ ∘ ⟨ (λg ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)))) , _ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ + -- eval′ ∘ ((λg ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)))) ⁂ id) ∘ ⟨ id , _ ⟩ ≈⟨ pullˡ β′ ⟩ + -- ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id))) ∘ ⟨ id , _ ⟩ ≈˘⟨ Elgot-Algebra.#-Uniformity A by-uni ⟩ + -- (Elgot-Algebra._# A) ((eval′ +₁ id) ∘ f) ∎ -- ⟨ ((π₁ +₁ id) ∘ h)#ᵃ , ((π₂ +₁ id) ∘ h)#ᵇ ⟩ + -- where + -- by-uni : (id +₁ ⟨ id , _ ⟩) ∘ ((eval′ +₁ id) ∘ f) ≈ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)) ∘ ⟨ id , _ ⟩ + -- by-uni = begin + -- (id +₁ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩) ∘ ((eval′ +₁ id) ∘ f) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ + -- (eval′ +₁ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩) ∘ f ≈˘⟨ sym-assoc ○ sym-assoc ○ (sym (+-unique by-inj₁ by-inj₂)) ⟩∘⟨refl ⟩ + -- (eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩ ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ refl assoc) ⟩ + -- (eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ ⟨ id ∘ f , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ∘ f ⟩ ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (⟨⟩-cong₂ refl (Elgot-Algebra.#-Fixpoint B))) ⟩ + -- (eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ ⟨ id ∘ f , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈˘⟨ pullʳ (pullʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ id-comm identityˡ)) ⟩ + -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈˘⟨ (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id π₁ id)))) ⟩∘⟨refl ⟩ + -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ⁂ id) ∘ (f ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩∘⟨refl ⟩ + -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎ + -- where + -- by-inj₁ : (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₁ ≈ i₁ ∘ eval′ + -- by-inj₁ = begin + -- (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₁ ≈⟨ pullʳ ⟨⟩∘ ⟩ + -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id ∘ i₁ , ([ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id)) ∘ i₁ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ id-comm-sym (pullʳ inject₁ ○ pullˡ inject₁ ○ identityˡ)) ⟩ + -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ i₁ ∘ id , π₂ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ refl identityˡ) ⟩ + -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ (i₁ ⁂ id) ∘ ⟨ id , π₂ ⟩ ≈⟨ pullʳ (pullʳ (pullˡ distributeʳ⁻¹-i₁)) ⟩ + -- (eval′ +₁ id) ∘ (π₁ ⁂ id +₁ id ⁂ id) ∘ i₁ ∘ ⟨ id , π₂ ⟩ ≈⟨ refl⟩∘⟨ (pullˡ +₁∘i₁) ⟩ + -- (eval′ +₁ id) ∘ (i₁ ∘ (π₁ ⁂ id)) ∘ ⟨ id , π₂ ⟩ ≈⟨ pullˡ (pullˡ +₁∘i₁) ⟩ + -- ((i₁ ∘ eval′) ∘ (π₁ ⁂ id)) ∘ ⟨ id , π₂ ⟩ ≈⟨ cancelʳ (⁂∘⟨⟩ ○ (⟨⟩-cong₂ identityʳ identityˡ) ○ ⟨⟩-unique identityʳ identityʳ) ⟩ + -- i₁ ∘ eval′ ∎ + -- by-inj₂ : (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₂ ≈ i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ + -- by-inj₂ = begin + -- (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₂ ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ id-comm-sym (pullʳ inject₂)) ⟩ + -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ i₂ ∘ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ i₂ ∘ id ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ identityʳ ○ inject₂)) ⟩ + -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ i₂ ∘ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ refl identityˡ) ⟩ + -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ (i₂ ⁂ id) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ pullʳ (pullʳ (pullˡ distributeʳ⁻¹-i₂)) ⟩ + -- (eval′ +₁ id) ∘ (π₁ ⁂ id +₁ id ⁂ id) ∘ i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ refl⟩∘⟨ (pullˡ inject₂) ⟩ + -- (eval′ +₁ id) ∘ (i₂ ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ pullˡ (pullˡ inject₂) ⟩ + -- ((i₂ ∘ id) ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ (cancelʳ (identityˡ ○ ⟨⟩-unique id-comm id-comm)) ⟩∘⟨refl ⟩ + -- i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎ + -- < CanonicalCartesianClosed.curry cccc {A} {B} {C} f > = λg < f > + -- preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = begin + -- λg < f > ∘ g #ᵃ ≈⟨ subst ⟩ + -- λg (< f > ∘ (g #ᵃ ⁂ id)) ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- λg (< f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩) ≈⟨ λ-cong (preserves f) ⟩ + -- λg (((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ) ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- {! !} ≈⟨ {! !} ⟩ + -- λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) #ᶜ) ∎ -- where -- open Elgot-Algebra A using () renaming (_# to _#ᵃ; #-Uniformity to #ᵃ-Uniformity) -- open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) -- open Elgot-Algebra C using () renaming (_# to _#ᶜ; #-resp-≈ to #ᶜ-resp-≈) - -- by-π₁ : π₁ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈ g #ᵃ ∘ π₁ - -- by-π₁ = project₁ ○ #ᵃ-Uniformity by-uni - -- where - -- by-uni : (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈ g ∘ π₁ - -- by-uni = begin - -- (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ - -- (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ distributeʳ⁻¹-π₁ ⟩ - -- π₁ ∘ (g ⁂ id) ≈⟨ project₁ ⟩ - -- g ∘ π₁ ∎ - -- by-π₂ : π₂ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈ id ∘ π₂ - -- by-π₂ = begin - -- π₂ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈⟨ project₂ ⟩ - -- ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ≈⟨ #ᵇ-Uniformity by-uni ⟩ - -- {! !} #ᵇ ∘ π₂ ≈⟨ {! !} ⟩ - -- {! !} ≈⟨ {! !} ⟩ - -- {! !} ≈⟨ {! !} ⟩ - -- {! !} ≈⟨ {! !} ⟩ - -- id ∘ π₂ ∎ - -- where - -- by-uni : (id +₁ π₂) ∘ (π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)) ≈ {! !} ∘ π₂ - -- by-uni = begin - -- {! !} ≈⟨ {! !} ⟩ - -- {! !} ≈⟨ {! !} ⟩ - -- {! !} ≈⟨ {! !} ⟩ - -- {! !} ≈⟨ {! !} ⟩ - -- {! !} ∎ - CanonicalCartesianClosed.eval-comp cccc {A} {B} {C} {f} = β′ - CanonicalCartesianClosed.curry-unique cccc {A} {B} {C} {f} {g} eq = λ-unique′ eq + -- -- uniqueness : ∀ + -- -- Elgot-Algebra-Morphism.preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = λ-unique′ (begin + -- -- eval′ ∘ ((λg < f > ∘ g #ᵃ) ⁂ id) ≈⟨ refl⟩∘⟨ ⁂-cong₂ subst refl ⟩ + -- -- eval′ ∘ ((λg (< f > ∘ (g #ᵃ ⁂ id))) ⁂ id) ≈⟨ β′ ⟩ + -- -- < f > ∘ (g #ᵃ ⁂ id) ≈⟨ refl⟩∘⟨ (⟨⟩-unique by-π₁ by-π₂) ⟩ + -- -- < f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈⟨ Elgot-Algebra-Morphism.preserves f ⟩ + -- -- ((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ ≈˘⟨ #ᶜ-resp-≈ (refl⟩∘⟨ assoc ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩ + -- -- ((eval′ +₁ id) ∘ (((λg < f > ⁂ id) +₁ (id ⁂ id)) ∘ distributeʳ⁻¹) ∘ (g ⁂ id)) #ᶜ ≈˘⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (λg < f >) id)))) ⟩ + -- -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg < f > +₁ id) ⁂ id) ∘ (g ⁂ id)) #ᶜ ≈⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩ + -- -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) #ᶜ ∎) + -- -- where + -- -- open Elgot-Algebra A using () renaming (_# to _#ᵃ; #-Uniformity to #ᵃ-Uniformity) + -- -- open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) + -- -- open Elgot-Algebra C using () renaming (_# to _#ᶜ; #-resp-≈ to #ᶜ-resp-≈) + -- -- by-π₁ : π₁ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈ g #ᵃ ∘ π₁ + -- -- by-π₁ = project₁ ○ #ᵃ-Uniformity by-uni + -- -- where + -- -- by-uni : (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈ g ∘ π₁ + -- -- by-uni = begin + -- -- (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ + -- -- (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ distributeʳ⁻¹-π₁ ⟩ + -- -- π₁ ∘ (g ⁂ id) ≈⟨ project₁ ⟩ + -- -- g ∘ π₁ ∎ + -- -- by-π₂ : π₂ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈ id ∘ π₂ + -- -- by-π₂ = begin + -- -- π₂ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈⟨ project₂ ⟩ + -- -- ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ≈⟨ #ᵇ-Uniformity by-uni ⟩ + -- -- {! !} #ᵇ ∘ π₂ ≈⟨ {! !} ⟩ + -- -- {! !} ≈⟨ {! !} ⟩ + -- -- {! !} ≈⟨ {! !} ⟩ + -- -- {! !} ≈⟨ {! !} ⟩ + -- -- id ∘ π₂ ∎ + -- -- where + -- -- by-uni : (id +₁ π₂) ∘ (π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)) ≈ {! !} ∘ π₂ + -- -- by-uni = begin + -- -- {! !} ≈⟨ {! !} ⟩ + -- -- {! !} ≈⟨ {! !} ⟩ + -- -- {! !} ≈⟨ {! !} ⟩ + -- -- {! !} ≈⟨ {! !} ⟩ + -- -- {! !} ∎ + -- CanonicalCartesianClosed.eval-comp cccc {A} {B} {C} {f} = β′ + -- CanonicalCartesianClosed.curry-unique cccc {A} {B} {C} {f} {g} eq = λ-unique′ eq - Elgot-CCC : CartesianClosed Elgot-Algebras - Elgot-CCC = Equivalence.fromCanonical Elgot-Algebras cccc + -- Elgot-CCC : CartesianClosed Elgot-Algebras + -- Elgot-CCC = Equivalence.fromCanonical Elgot-Algebras cccc ``` diff --git a/agda/src/Monad/Instance/K/Commutative.lagda.md b/agda/src/Monad/Instance/K/Commutative.lagda.md index 08ec99f..fc20b1a 100644 --- a/agda/src/Monad/Instance/K/Commutative.lagda.md +++ b/agda/src/Monad/Instance/K/Commutative.lagda.md @@ -24,7 +24,7 @@ open import Category.Construction.ElgotAlgebras {C = C} open Cat cocartesian open import Algebra.Elgot cocartesian open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF) -open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra) +open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra; IsStableFreeElgotAlgebraˡ; isStable⇒isStableˡ) open Equiv open HomReasoning @@ -43,14 +43,18 @@ The proof is analogous to the ones for strength, the relevant diagram is: open monadK using (μ) open kleisliK using (extend) open strongK using (strengthen) -open IsStableFreeElgotAlgebra using (♯-law; ♯-preserving; ♯-unique; ♯ˡ-unique; ♯ˡ-preserving; ♯ˡ-law) +open IsStableFreeElgotAlgebra using (♯-law; ♯-preserving; ♯-unique) +open IsStableFreeElgotAlgebraˡ using (♯ˡ-unique; ♯ˡ-preserving; ♯ˡ-law) open Elgot-Algebra using (#-Uniformity; #-Fixpoint; #-Compositionality; #-Diamond; #-resp-≈) + + -- some helper definitions to make our life easier private + stableˡ = λ X → isStable⇒isStableˡ (freealgebras X) (stable X) η = λ Z → FreeObject.η (freealgebras Z) _♯ = λ {A X Y} f → IsStableFreeElgotAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f - _♯ˡ = λ {A X Y} f → IsStableFreeElgotAlgebra.[_,_]♯ˡ {Y = X} (stable X) {X = A} (algebras Y) f + _♯ˡ = λ {A X Y} f → IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ {Y = X} (stableˡ X) {X = A} (algebras Y) f _# = λ {A} {X} f → Elgot-Algebra._# (algebras A) {X = X} f -- First we establish some facts about σ @@ -331,8 +335,8 @@ 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 #) ≈⟨ 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 ⁂ 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 diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md index fa9d9ad..f725555 100644 --- a/agda/src/Monad/Instance/Setoids/K.lagda.md +++ b/agda/src/Monad/Instance/Setoids/K.lagda.md @@ -15,11 +15,12 @@ open Eq using (_≡_) renaming (sym to ≣-sym; refl to ≣-refl; trans to ≣-t open import Categories.FreeObjects.Free open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) open import Data.Product.Function.NonDependent.Setoid using (proj₁ₛ) -open import Categories.Category.Instance.Properties.Setoids.Choice using () open import Data.Product.Relation.Binary.Pointwise.NonDependent open import Data.Product open import Category.Ambient using (Ambient) +open import Categories.Category.CartesianClosed open import Categories.Category.Instance.Setoids +open import Categories.Category.Instance.Properties.Setoids.CCC using (Setoids-CCC) ``` --> @@ -34,6 +35,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where open import Monad.Instance.K (setoidAmbient {ℓ}) open import Algebra.Elgot cocartesian open import Algebra.Elgot.Free cocartesian + open import Algebra.Elgot.Stable distributive open import Category.Construction.ElgotAlgebras {C = Setoids ℓ ℓ} open Cat cocartesian open import Monad.PreElgot (setoidAmbient {ℓ}) @@ -385,7 +387,9 @@ module Monad.Instance.Setoids.K {ℓ : Level} where iter-id {now x} = ≈-refl A iter-id {later x} = later≈ (iter-id′ {force x}) + open CartesianClosed (Setoids-CCC ℓ) renaming (exp to setoid-exp) + open import Algebra.Elgot.Properties distributive setoid-exp using (free-isStableˡ) delayK : MonadK - delayK = record { freealgebras = freeAlgebra ; stable = {! !} } + delayK = record { freealgebras = freeAlgebra ; stable = λ X → isStableˡ⇒isStable (freeAlgebra X) (free-isStableˡ (freeAlgebra X)) } ``` \ No newline at end of file