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

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

Browse source
This commit is contained in:
Leon Vatthauer 2024-02-05 18:12:58 +01:00
parent 840e02b842
commit 161ceabcda
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
5 changed files with 254 additions and 183 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
agda/src/Algebra/Elgot/Properties.lagda.md
View file

@ -33,8 +33,9 @@ module Algebra.Elgot.Properties {o ℓ e} {C : Category o ℓ e} (distributive :
open Cartesian cartesian open Cartesian cartesian
open BinaryProducts products hiding (η) renaming (unique to ⟨⟩-unique) open BinaryProducts products hiding (η) renaming (unique to ⟨⟩-unique)
open Cocartesian cocartesian open Cocartesian cocartesian
ccc : CartesianClosed C private
ccc = record { cartesian = cartesian ; exp = expos } ccc : CartesianClosed C
ccc = record { cartesian = cartesian ; exp = expos }
open CartesianClosed ccc hiding (exp; cartesian) 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.Free cocartesian
open import Algebra.Elgot.Stable distributive open import Algebra.Elgot.Stable distributive
open CartesianClosed Elgot-CCC using () renaming (λg to λg#; _^_ to _^#_)
open Elgot-Algebra-Morphism renaming (h to <_>) open Elgot-Algebra-Morphism renaming (h to <_>)
stable : ∀ {Y} (fe : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebraˡ fe free-isStableˡ : ∀ {Y} (fe : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebraˡ fe
IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (stable {Y} fe) {X} A f = (eval′ ∘ (< FreeObject._* fe {B^A-Helper {A} {X}} (λg f) > ⁂ id)) IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (free-isStableˡ {Y} fe) {X} A f = (eval′ ∘ (< FreeObject._* fe {B^A-Helper {A} {X}} (λg f) > ⁂ id))
where open FreeObject fe 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) ≈⟨ pullʳ ⁂∘⁂ ⟩
eval′ ∘ ((< (λg f)* > ∘ η) ⁂ id ∘ id) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (*-lift (λg f)) identity²) ⟩ eval′ ∘ ((< (λg f)* > ∘ η) ⁂ id ∘ id) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (*-lift (λg f)) identity²) ⟩
eval′ ∘ (λg f ⁂ id) ≈⟨ β′ ⟩ eval′ ∘ (λg f ⁂ id) ≈⟨ β′ ⟩
f ∎) f ∎)
where open FreeObject fe 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)* > ⁂ id)) ∘ (h #ʸ ⁂ id) ≈⟨ pullʳ ⁂∘⁂ ⟩
eval′ ∘ (< (λg f)* > ∘ h #ʸ ⁂ id ∘ id) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (preserves ((λg f)*)) identity²) ⟩ eval′ ∘ (< (λg f)* > ∘ h #ʸ ⁂ id ∘ id) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (preserves ((λg f)*)) identity²) ⟩
eval′ ∘ (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((< (λg f)* > +₁ id) ∘ h ⁂ id)) #ᵇ) ⁂ id) ≈⟨ β′ ⟩ 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 FreeObject fe renaming (FX to KY)
open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-resp-≈ to #ᵇ-resp-≈) open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-resp-≈ to #ᵇ-resp-≈)
open Elgot-Algebra KY using () renaming (_# to _#ʸ) open Elgot-Algebra KY using () renaming (_# to _#ʸ)
IsStableFreeElgotAlgebraˡ.♯ˡ-unique (stable {Y} fe) {X} {B} f g eq₁ eq₂ = sym (begin IsStableFreeElgotAlgebraˡ.♯ˡ-unique (free-isStableˡ {Y} fe) {X} {B} f g eq₁ eq₂ = λ-inj (begin
eval′ ∘ (< (λg f)* > ⁂ id) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (*-cong (λ-cong eq₁)) refl) ⟩ λg g ≈⟨ *-uniq (λg f) (record { h = λg g ; preserves = λ {D} {h} → begin
eval′ ∘ (< (λg (g ∘ (η ⁂ id)))* > ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂-cong₂ (*-cong subst) refl) ⟩ λg g ∘ (h #ʸ) ≈⟨ subst ⟩
eval′ ∘ (< (λg g ∘ η)* > ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂-cong₂ (*-uniq (λg g ∘ η) (record { h = λg g ; preserves = {! !} }) refl) refl) ⟩ λg (g ∘ (h #ʸ ⁂ id)) ≈⟨ λ-cong (eq₂ h) ⟩
eval′ ∘ (λg g ⁂ id) ≈⟨ β′ ⟩ λg (((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ) ≈˘⟨ λ-cong (#ᵇ-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ (elimʳ (⟨⟩-unique id-comm id-comm))))) ⟩
g ∎) λ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 where
open FreeObject fe renaming (FX to KY) open FreeObject fe renaming (FX to KY)
open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-resp-≈ to #ᵇ-resp-≈) open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-resp-≈ to #ᵇ-resp-≈)

175
agda/src/Algebra/Elgot/Stable.lagda.md
View file

@ -61,7 +61,6 @@ Stable free Elgot algebras have an additional universal iteration preserving mor
open Elgot-Algebra FY using (_#) open Elgot-Algebra FY using (_#)
field 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 [_,_]♯ : ∀ {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 ⁂ η) ♯-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)) ♯-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 ⁂ η) → f ≈ g ∘ (id ⁂ η)
→ (∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (id ⁂ h #) ≈ Elgot-Algebra._# B ((g +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))) → (∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (id ⁂ h #) ≈ Elgot-Algebra._# B ((g +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)))
→ g ≈ [ B , f ]♯ → 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 record StableFreeElgotAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where
field field
@ -130,9 +195,3 @@ Stable free Elgot algebras have an additional universal iteration preserving mor
open IsStableFreeElgotAlgebra isStableFreeElgotAlgebra public open IsStableFreeElgotAlgebra isStableFreeElgotAlgebra public
``` ```
In a cartesian closed category stability is derivable
```agda
-- TODO
```

209
agda/src/Category/Construction/ElgotAlgebras.lagda.md
View file

@ -316,113 +316,114 @@ module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} wher
open Elgot-Algebra-Morphism renaming (h to <_>) open Elgot-Algebra-Morphism renaming (h to <_>)
cccc : CanonicalCartesianClosed Elgot-Algebras -- cccc : CanonicalCartesianClosed Elgot-Algebras
CanonicalCartesianClosed.⊤ cccc = Terminal.⊤ Terminal-Elgot-Algebras -- CanonicalCartesianClosed.⊤ cccc = Terminal.⊤ Terminal-Elgot-Algebras
CanonicalCartesianClosed._×_ cccc X Y = A×B-Helper {X} {Y} -- CanonicalCartesianClosed._×_ cccc X Y = A×B-Helper {X} {Y}
CanonicalCartesianClosed.! cccc = Terminal.! Terminal-Elgot-Algebras -- 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} = 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.⟨_,_⟩ cccc {X} {Y} {Z} f g = Product.⟨_,_⟩ (Product-Elgot-Algebras Y Z) f g
CanonicalCartesianClosed.!-unique cccc = Terminal.!-unique Terminal-Elgot-Algebras -- 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.π₂-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.⟨,⟩-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} -- 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.h) (CanonicalCartesianClosed.eval cccc {A} {B}) = eval′
(Elgot-Algebra-Morphism.preserves) (CanonicalCartesianClosed.eval cccc {A} {B}) {X} {f} = begin -- (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)))) , _ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
eval′ ∘ ((λg ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)))) ⁂ id) ∘ ⟨ id , _ ⟩ ≈⟨ pullˡ β′ ⟩ -- 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) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id))) ∘ ⟨ id , _ ⟩ ≈˘⟨ Elgot-Algebra.#-Uniformity A by-uni ⟩
(Elgot-Algebra._# A) ((eval′ +₁ id) ∘ f) ∎ -- ⟨ ((π₁ +₁ id) ∘ h)#ᵃ , ((π₂ +₁ id) ∘ h)#ᵇ ⟩ -- (Elgot-Algebra._# A) ((eval′ +₁ id) ∘ f) ∎ -- ⟨ ((π₁ +₁ id) ∘ h)#ᵃ , ((π₂ +₁ id) ∘ h)#ᵇ ⟩
where -- where
by-uni : (id +₁ ⟨ id , _ ⟩) ∘ ((eval′ +₁ id) ∘ f) ≈ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)) ∘ ⟨ id , _ ⟩ -- by-uni : (id +₁ ⟨ id , _ ⟩) ∘ ((eval′ +₁ id) ∘ f) ≈ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)) ∘ ⟨ id , _ ⟩
by-uni = begin -- by-uni = begin
(id +₁ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩) ∘ ((eval′ +₁ id) ∘ f) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ -- (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 , (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 , [ 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 , [ 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ʳ⁻¹) ∘ ⟨ 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) ∘ ((π₁ ⁂ 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) ⁂ 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) ⟩ ∎ -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎
where -- where
by-inj₁ : (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₁ ≈ i₁ ∘ eval′ -- by-inj₁ : (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₁ ≈ i₁ ∘ eval′
by-inj₁ = begin -- 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 , [ 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ʳ⁻¹)) ∘ ⟨ 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 , π₂ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ refl identityˡ) ⟩
((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ (i₁ ⁂ id) ∘ ⟨ id , π₂ ⟩ ≈⟨ pullʳ (pullʳ (pullˡ distributeʳ⁻¹-i₁)) ⟩ -- ((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) ∘ (π₁ ⁂ id +₁ id ⁂ id) ∘ i₁ ∘ ⟨ id , π₂ ⟩ ≈⟨ refl⟩∘⟨ (pullˡ +₁∘i₁) ⟩
(eval′ +₁ id) ∘ (i₁ ∘ (π₁ ⁂ id)) ∘ ⟨ id , π₂ ⟩ ≈⟨ pullˡ (pullˡ +₁∘i₁) ⟩ -- (eval′ +₁ id) ∘ (i₁ ∘ (π₁ ⁂ id)) ∘ ⟨ id , π₂ ⟩ ≈⟨ pullˡ (pullˡ +₁∘i₁) ⟩
((i₁ ∘ eval′) ∘ (π₁ ⁂ id)) ∘ ⟨ id , π₂ ⟩ ≈⟨ cancelʳ (⁂∘⟨⟩ ○ (⟨⟩-cong₂ identityʳ identityˡ) ○ ⟨⟩-unique identityʳ identityʳ) ⟩ -- ((i₁ ∘ eval′) ∘ (π₁ ⁂ id)) ∘ ⟨ id , π₂ ⟩ ≈⟨ cancelʳ (⁂∘⟨⟩ ○ (⟨⟩-cong₂ identityʳ identityˡ) ○ ⟨⟩-unique identityʳ identityʳ) ⟩
i₁ ∘ eval′ ∎ -- 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₂ : (((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 -- 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ʳ⁻¹)) ∘ ⟨ 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 , [ 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 , (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) ∘ 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) ∘ (π₁ ⁂ 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₂) ⟩ -- (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) ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ (cancelʳ (identityˡ ○ ⟨⟩-unique id-comm id-comm)) ⟩∘⟨refl ⟩
i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎ -- i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎
< CanonicalCartesianClosed.curry cccc {A} {B} {C} f > = λg < f > -- < CanonicalCartesianClosed.curry cccc {A} {B} {C} f > = λg < f >
preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = begin -- preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = begin
λg < f > ∘ g #ᵃ ≈⟨ subst ⟩ -- λg < f > ∘ g #ᵃ ≈⟨ subst ⟩
λg (< f > ∘ (g #ᵃ ⁂ id)) ≈⟨ {! !} ⟩ -- λg (< f > ∘ (g #ᵃ ⁂ id)) ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩ -- {! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩ -- {! !} ≈⟨ {! !} ⟩
λg (< f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩) ≈⟨ λ-cong (preserves f) ⟩ -- λg (< f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩) ≈⟨ λ-cong (preserves f) ⟩
λg (((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ) ≈⟨ {! !} ⟩ -- λg (((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ) ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩ -- {! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩ -- {! !} ≈⟨ {! !} ⟩
λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ 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)) #ᶜ ∎)
-- where -- where
-- open Elgot-Algebra A using () renaming (_# to _#ᵃ; #-Uniformity to #ᵃ-Uniformity) -- open Elgot-Algebra A using () renaming (_# to _#ᵃ; #-Uniformity to #ᵃ-Uniformity)
-- open Elgot-Algebra B 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-≈) -- open Elgot-Algebra C using () renaming (_# to _#ᶜ; #-resp-≈ to #ᶜ-resp-≈)
-- by-π₁ : π₁ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈ g #ᵃ ∘ π₁ -- -- uniqueness : ∀
-- by-π₁ = project₁ ○ #ᵃ-Uniformity by-uni -- -- Elgot-Algebra-Morphism.preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = λ-unique′ (begin
-- where -- -- eval′ ∘ ((λg < f > ∘ g #ᵃ) ⁂ id) ≈⟨ refl⟩∘⟨ ⁂-cong₂ subst refl ⟩
-- by-uni : (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈ g ∘ π₁ -- -- eval′ ∘ ((λg (< f > ∘ (g #ᵃ ⁂ id))) ⁂ id) ≈⟨ β′ ⟩
-- by-uni = begin -- -- < f > ∘ (g #ᵃ ⁂ id) ≈⟨ refl⟩∘⟨ (⟨⟩-unique by-π₁ by-π₂) ⟩
-- (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ -- -- < f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈⟨ Elgot-Algebra-Morphism.preserves f ⟩
-- (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ distributeʳ⁻¹-π₁ ⟩ -- -- ((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ ≈˘⟨ #ᶜ-resp-≈ (refl⟩∘⟨ assoc ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩
-- π₁ ∘ (g ⁂ id) ≈⟨ project₁ ⟩ -- -- ((eval′ +₁ id) ∘ (((λg < f > ⁂ id) +₁ (id ⁂ id)) ∘ distributeʳ⁻¹) ∘ (g ⁂ id)) #ᶜ ≈˘⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (λg < f >) id)))) ⟩
-- g ∘ π₁ ∎ -- -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg < f > +₁ id) ⁂ id) ∘ (g ⁂ id)) #ᶜ ≈⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩
-- by-π₂ : π₂ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈ id ∘ π₂ -- -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) #ᶜ ∎)
-- by-π₂ = begin -- -- where
-- π₂ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈⟨ project₂ ⟩ -- -- open Elgot-Algebra A using () renaming (_# to _#ᵃ; #-Uniformity to #ᵃ-Uniformity)
-- ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ≈⟨ #ᵇ-Uniformity by-uni ⟩ -- -- 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
-- id ∘ π₂ ∎ -- -- by-uni : (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈ g ∘ π₁
-- where -- -- by-uni = begin
-- by-uni : (id +₁ π₂) ∘ (π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)) ≈ {! !} ∘ π₂ -- -- (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩
-- by-uni = begin -- -- (π₁ +₁ π₁) ∘ 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₂ ⟩
CanonicalCartesianClosed.eval-comp cccc {A} {B} {C} {f} = β′ -- -- ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ≈⟨ #ᵇ-Uniformity by-uni ⟩
CanonicalCartesianClosed.curry-unique cccc {A} {B} {C} {f} {g} eq = λ-unique′ eq -- -- {! !} #ᵇ ∘ π₂ ≈⟨ {! !} ⟩
-- -- {! !} ≈⟨ {! !} ⟩
-- -- {! !} ≈⟨ {! !} ⟩
-- -- {! !} ≈⟨ {! !} ⟩
-- -- 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 : CartesianClosed Elgot-Algebras
Elgot-CCC = Equivalence.fromCanonical Elgot-Algebras cccc -- Elgot-CCC = Equivalence.fromCanonical Elgot-Algebras cccc
``` ```

14
agda/src/Monad/Instance/K/Commutative.lagda.md
View file

@ -24,7 +24,7 @@ open import Category.Construction.ElgotAlgebras {C = C}
open Cat cocartesian open Cat cocartesian
open import Algebra.Elgot cocartesian open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF) 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 Equiv
open HomReasoning open HomReasoning
@ -43,14 +43,18 @@ The proof is analogous to the ones for strength, the relevant diagram is:
open monadK using (μ) open monadK using (μ)
open kleisliK using (extend) open kleisliK using (extend)
open strongK using (strengthen) 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-≈) open Elgot-Algebra using (#-Uniformity; #-Fixpoint; #-Compositionality; #-Diamond; #-resp-≈)
-- some helper definitions to make our life easier -- some helper definitions to make our life easier
private private
stableˡ = λ X → isStable⇒isStableˡ (freealgebras X) (stable X)
η = λ Z → FreeObject.η (freealgebras Z) η = λ 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 Y} f → IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ {Y = X} (stableˡ X) {X = A} (algebras Y) f
_# = λ {A} {X} f → Elgot-Algebra._# (algebras A) {X = X} f _# = λ {A} {X} f → Elgot-Algebra._# (algebras A) {X = X} f
-- First we establish some facts about σ -- 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 : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
comm₄ {Z} h = begin comm₄ {Z} h = begin
(μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈⟨ sym-assoc ⟩∘⟨refl ⟩ (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈⟨ sym-assoc ⟩∘⟨refl ⟩
ψ ∘ (idC ⁂ h #) ≈⟨ ♯ˡ-unique (stable _) (τ (X , Y) ∘ (idC ⁂ (h #))) (ψ ∘ (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 ⁂ 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) ⟩ ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc refl) ⟩∘⟨refl) ⟩
((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎ ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
where where

8
agda/src/Monad/Instance/Setoids/K.lagda.md
View file

@ -15,11 +15,12 @@ open Eq using (_≡_) renaming (sym to ≣-sym; refl to ≣-refl; trans to ≣-t
open import Categories.FreeObjects.Free open import Categories.FreeObjects.Free
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Data.Product.Function.NonDependent.Setoid using (proj₁ₛ) 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.Relation.Binary.Pointwise.NonDependent
open import Data.Product open import Data.Product
open import Category.Ambient using (Ambient) open import Category.Ambient using (Ambient)
open import Categories.Category.CartesianClosed
open import Categories.Category.Instance.Setoids 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 Monad.Instance.K (setoidAmbient {ℓ})
open import Algebra.Elgot cocartesian open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian open import Algebra.Elgot.Free cocartesian
open import Algebra.Elgot.Stable distributive
open import Category.Construction.ElgotAlgebras {C = Setoids ℓ ℓ} open import Category.Construction.ElgotAlgebras {C = Setoids ℓ ℓ}
open Cat cocartesian open Cat cocartesian
open import Monad.PreElgot (setoidAmbient {ℓ}) open import Monad.PreElgot (setoidAmbient {ℓ})
@ -385,7 +387,9 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
iter-id {now x} = ≈-refl A iter-id {now x} = ≈-refl A
iter-id {later x} = later≈ (iter-id′ {force x}) 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 : MonadK
delayK = record { freealgebras = freeAlgebra ; stable = {! !} } delayK = record { freealgebras = freeAlgebra ; stable = λ X → isStableˡ⇒isStable (freeAlgebra X) (free-isStableˡ (freeAlgebra X)) }
``` ```