diff --git a/public/Monad.Instance.Delay.html b/public/Monad.Instance.Delay.html index b9a9fca..21d3ca7 100644 --- a/public/Monad.Instance.Delay.html +++ b/public/Monad.Instance.Delay.html @@ -38,9 +38,11 @@ open import Categories.Category.Construction.F-Coalgebras open import Categories.Functor.Coalgebra open import Categories.Functor -open import Categories.Monad.Construction.Kleisli -import Categories.Morphism as M -import Categories.Morphism.Reasoning as MR +open import Categories.Functor.Algebra +open import Categories.Monad.Construction.Kleisli +open import Categories.Category.Construction.F-Coalgebras +import Categories.Morphism as M +import Categories.Morphism.Reasoning as MR -->

Summary

This file introduces the delay monad D

@@ -52,61 +54,108 @@ D is commutative

Code

-
module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
-  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
-  open Cocartesian (Extensive.cocartesian extensive)
-  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
-  open BinaryProducts products
+
module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
+  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
+  open Cocartesian (Extensive.cocartesian extensive)
+  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
+  open BinaryProducts products
 
-  open M C
-  open MR C
-  open Equiv
-  open HomReasoning
+  open M C
+  open MR C
+  open Equiv
+  open HomReasoning
+  open CoLambek
 

 
Proposition
 1: Characterization of the delay monad
 D

-
  record DelayMonad (D : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
-    open Functor D using () renaming (F₀ to D₀; F₁ to D₁)
+
First I postulate the Functor D, maybe I should derive it…
+TODO: - how to define using final coalgebra(s)? - DX
+can be defined as retract of infinite streams, how? - how to express
+Theorem 8 in agda?

+
  record DelayFunctor : Set (o ⊔ ℓ ⊔ e) where
+    field
+      D : Endofunctor C
 
-    field
-      now : ∀ {X} → X ⇒ D₀ X
-      later : ∀ {X} → D₀ X ⇒ D₀ X
-      isIso : ∀ {X} → IsIso [ now {X} , later {X} ]
+    open Functor D public renaming (F₀ to D₀; F₁ to D₁)
+
+    field
+      now : ∀ {X} → X ⇒ D₀ X
+      later : ∀ {X} → D₀ X ⇒ D₀ X
+      isIso : ∀ {X} → IsIso [ now {X} , later {X} ]
+
+    out : ∀ {X} → D₀ X ⇒ X + D₀ X
+    out {X} = IsIso.inv (isIso {X})
+
+    field
+      coit : ∀ {X Y} → Y ⇒ X + Y → Y ⇒ D₀ X
+      coit-law : ∀ {X Y} {f : Y ⇒ X + Y} → out ∘ (coit f) ≈ (idC +₁ (coit f)) ∘ f
+

+
Now let’s define the monad:

+
  record DelayMonad : Set (o ⊔ ℓ ⊔ e) where
+    field
+      D : DelayFunctor
+    open DelayFunctor D
+
+    field
+      _* : ∀ {X Y} → X ⇒ D₀ Y → D₀ X ⇒ D₀ Y
+      *-law : ∀ {X Y} {f : X ⇒ D₀ Y} → out ∘ (f *) ≈ [ out ∘ f , i₂ ∘ (f *) ] ∘ out
+      *-unique : ∀ {X Y} (f : X ⇒ D₀ Y) (h : D₀ X ⇒ D₀ Y) → h ≈ f *
+      *-resp-≈ : ∀ {X Y} {f h : X ⇒ D₀ Y} → f ≈ h → f * ≈ h * 
+
+    unitLaw : ∀ {X} → out {X} ∘ now {X} ≈ i₁
+    unitLaw = begin 
+      out ∘ now ≈⟨ refl⟩∘⟨ sym inject₁ ⟩ 
+      out ∘ [ now , later ] ∘ i₁ ≈⟨ cancelˡ (IsIso.isoˡ isIso) ⟩
+      i₁ ∎
+
+    toMonad : KleisliTriple C
+    toMonad = record
+      { F₀ = D₀
+      ; unit = now
+      ; extend = _*
+      ; identityʳ = λ {X} {Y} {k} → begin 
+        k * ∘ now ≈⟨ introˡ (IsIso.isoʳ isIso) ⟩∘⟨refl ⟩ 
+        (([ now , later ] ∘ out) ∘ k *) ∘ now ≈⟨ pullʳ *-law ⟩∘⟨refl ⟩
+        ([ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitLaw) ⟩
+        [ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩
+        [ now , later ] ∘ out ∘ k ≈⟨ cancelˡ (IsIso.isoʳ isIso) ⟩
+        k ∎
+      ; identityˡ = λ {X} → sym (*-unique now idC)
+      ; assoc = λ {X} {Y} {Z} {f} {g} → sym (*-unique ((g *) ∘ f) ((g *) ∘ (f *)))
+      ; sym-assoc = λ {X} {Y} {Z} {f} {g} → *-unique ((g *) ∘ f) ((g *) ∘ (f *))
+      ; extend-≈ = *-resp-≈
+      }
+

+
Definition 30:
+Search-Algebras

+
  record SearchAlgebra (DF : DelayFunctor) : Set (o ⊔ ℓ ⊔ e) where
+    open DelayFunctor DF
     
-    out : ∀ {X} → D₀ X ⇒ X + D₀ X
-    out {X} = IsIso.inv (isIso {X})
+    field
+      FA : F-Algebra D
 
-    field
-      _* : ∀ {X Y} → X ⇒ D₀ Y → D₀ X ⇒ D₀ Y
-      *-law : ∀ {X Y} {f : X ⇒ D₀ Y} → out ∘ (f *) ≈ [ out ∘ f , i₂ ∘ (f *) ] ∘ out
-      *-unique : ∀ {X Y} (f : X ⇒ D₀ Y) (h : D₀ X ⇒ D₀ Y) → h ≈ f *
-      *-resp-≈ : ∀ {X Y} {f h : X ⇒ D₀ Y} → f ≈ h → f * ≈ h * 
+    open F-Algebra FA
 
-    unitLaw : ∀ {X} → out {X} ∘ now {X} ≈ i₁
-    unitLaw = begin 
-      out ∘ now ≈⟨ refl⟩∘⟨ sym inject₁ ⟩ 
-      out ∘ [ now , later ] ∘ i₁ ≈⟨ cancelˡ (IsIso.isoˡ isIso) ⟩
-      i₁ ∎
-
-    toMonad : KleisliTriple C
-    toMonad = record
-      { F₀ = D₀
-      ; unit = now
-      ; extend = _*
-      ; identityʳ = λ {X} {Y} {k} → begin 
-        k * ∘ now ≈⟨ introˡ (IsIso.isoʳ isIso) ⟩∘⟨refl ⟩ 
-        (([ now , later ] ∘ out) ∘ k *) ∘ now ≈⟨ pullʳ *-law ⟩∘⟨refl ⟩
-        ([ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitLaw) ⟩
-        [ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩
-        [ now , later ] ∘ out ∘ k ≈⟨ cancelˡ (IsIso.isoʳ isIso) ⟩
-        k ∎
-      ; identityˡ = λ {X} → sym (*-unique now idC)
-      ; assoc = λ {X} {Y} {Z} {f} {g} → sym (*-unique ((g *) ∘ f) ((g *) ∘ (f *)))
-      ; sym-assoc = λ {X} {Y} {Z} {f} {g} → *-unique ((g *) ∘ f) ((g *) ∘ (f *))
-      ; extend-≈ = *-resp-≈
-      }
+    field
+      now-id : α ∘ now ≈ idC    
+      later-same : α ∘ later ≈ α
+

+
Proposition
+31 : the category of uniform-iteration algebras coincides with the
+category of search-algebras

+
TODOs:

+
+
  record SearchAlgebras (DF : DelayFunctor) : Set (o ⊔ ℓ ⊔ e) where
+    open DelayFunctor DF
 

 
 
diff --git a/public/Monad.Instance.Delay.md b/public/Monad.Instance.Delay.md
index e9636c2..e9bbe41 100644
--- a/public/Monad.Instance.Delay.md
+++ b/public/Monad.Instance.Delay.md
@@ -11,9 +11,11 @@
 open import Categories.Category.Construction.F-Coalgebras
 open import Categories.Functor.Coalgebra
 open import Categories.Functor
-open import Categories.Monad.Construction.Kleisli
-import Categories.Morphism as M
-import Categories.Morphism.Reasoning as MR
+open import Categories.Functor.Algebra
+open import Categories.Monad.Construction.Kleisli
+open import Categories.Category.Construction.F-Coalgebras
+import Categories.Morphism as M
+import Categories.Morphism.Reasoning as MR
 
-->
 
 ## Summary
@@ -24,55 +26,102 @@ This file introduces the delay monad ***D***
 
 ## Code
 
-
module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
-  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
-  open Cocartesian (Extensive.cocartesian extensive)
-  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
-  open BinaryProducts products
+
module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
+  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
+  open Cocartesian (Extensive.cocartesian extensive)
+  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
+  open BinaryProducts products
 
-  open M C
-  open MR C
-  open Equiv
-  open HomReasoning
+  open M C
+  open MR C
+  open Equiv
+  open HomReasoning
+  open CoLambek
 
### *Proposition 1*: Characterization of the delay monad ***D***
-
  record DelayMonad (D : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
-    open Functor D using () renaming (F₀ to D₀; F₁ to D₁)
 
-    field
-      now : ∀ {X} → X ⇒ D₀ X
-      later : ∀ {X} → D₀ X ⇒ D₀ X
-      isIso : ∀ {X} → IsIso [ now {X} , later {X} ]
+First I postulate the Functor *D*, maybe I should derive it...
+**TODO**: 
+- how to define using final coalgebra(s)?
+- DX can be defined as retract of infinite streams, how?
+- how to express **Theorem 8** in agda?
+
+
  record DelayFunctor : Set (o ⊔ ℓ ⊔ e) where
+    field
+      D : Endofunctor C
+
+    open Functor D public renaming (F₀ to D₀; F₁ to D₁)
+
+    field
+      now : ∀ {X} → X ⇒ D₀ X
+      later : ∀ {X} → D₀ X ⇒ D₀ X
+      isIso : ∀ {X} → IsIso [ now {X} , later {X} ]
+
+    out : ∀ {X} → D₀ X ⇒ X + D₀ X
+    out {X} = IsIso.inv (isIso {X})
+
+    field
+      coit : ∀ {X Y} → Y ⇒ X + Y → Y ⇒ D₀ X
+      coit-law : ∀ {X Y} {f : Y ⇒ X + Y} → out ∘ (coit f) ≈ (idC +₁ (coit f)) ∘ f
+

+Now let's define the monad:
+
+
  record DelayMonad : Set (o ⊔ ℓ ⊔ e) where
+    field
+      D : DelayFunctor
+    open DelayFunctor D
+
+    field
+      _* : ∀ {X Y} → X ⇒ D₀ Y → D₀ X ⇒ D₀ Y
+      *-law : ∀ {X Y} {f : X ⇒ D₀ Y} → out ∘ (f *) ≈ [ out ∘ f , i₂ ∘ (f *) ] ∘ out
+      *-unique : ∀ {X Y} (f : X ⇒ D₀ Y) (h : D₀ X ⇒ D₀ Y) → h ≈ f *
+      *-resp-≈ : ∀ {X Y} {f h : X ⇒ D₀ Y} → f ≈ h → f * ≈ h * 
+
+    unitLaw : ∀ {X} → out {X} ∘ now {X} ≈ i₁
+    unitLaw = begin 
+      out ∘ now ≈⟨ refl⟩∘⟨ sym inject₁ ⟩ 
+      out ∘ [ now , later ] ∘ i₁ ≈⟨ cancelˡ (IsIso.isoˡ isIso) ⟩
+      i₁ ∎
+
+    toMonad : KleisliTriple C
+    toMonad = record
+      { F₀ = D₀
+      ; unit = now
+      ; extend = _*
+      ; identityʳ = λ {X} {Y} {k} → begin 
+        k * ∘ now ≈⟨ introˡ (IsIso.isoʳ isIso) ⟩∘⟨refl ⟩ 
+        (([ now , later ] ∘ out) ∘ k *) ∘ now ≈⟨ pullʳ *-law ⟩∘⟨refl ⟩
+        ([ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitLaw) ⟩
+        [ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩
+        [ now , later ] ∘ out ∘ k ≈⟨ cancelˡ (IsIso.isoʳ isIso) ⟩
+        k ∎
+      ; identityˡ = λ {X} → sym (*-unique now idC)
+      ; assoc = λ {X} {Y} {Z} {f} {g} → sym (*-unique ((g *) ∘ f) ((g *) ∘ (f *)))
+      ; sym-assoc = λ {X} {Y} {Z} {f} {g} → *-unique ((g *) ∘ f) ((g *) ∘ (f *))
+      ; extend-≈ = *-resp-≈
+      }
+

+### Definition 30: Search-Algebras
+
+
  record SearchAlgebra (DF : DelayFunctor) : Set (o ⊔ ℓ ⊔ e) where
+    open DelayFunctor DF
     
-    out : ∀ {X} → D₀ X ⇒ X + D₀ X
-    out {X} = IsIso.inv (isIso {X})
+    field
+      FA : F-Algebra D
 
-    field
-      _* : ∀ {X Y} → X ⇒ D₀ Y → D₀ X ⇒ D₀ Y
-      *-law : ∀ {X Y} {f : X ⇒ D₀ Y} → out ∘ (f *) ≈ [ out ∘ f , i₂ ∘ (f *) ] ∘ out
-      *-unique : ∀ {X Y} (f : X ⇒ D₀ Y) (h : D₀ X ⇒ D₀ Y) → h ≈ f *
-      *-resp-≈ : ∀ {X Y} {f h : X ⇒ D₀ Y} → f ≈ h → f * ≈ h * 
+    open F-Algebra FA
 
-    unitLaw : ∀ {X} → out {X} ∘ now {X} ≈ i₁
-    unitLaw = begin 
-      out ∘ now ≈⟨ refl⟩∘⟨ sym inject₁ ⟩ 
-      out ∘ [ now , later ] ∘ i₁ ≈⟨ cancelˡ (IsIso.isoˡ isIso) ⟩
-      i₁ ∎
+    field
+      now-id : α ∘ now ≈ idC    
+      later-same : α ∘ later ≈ α
+

+### Proposition 31 : the category of uniform-iteration algebras coincides with the category of search-algebras
+TODOs:
 
-    toMonad : KleisliTriple C
-    toMonad = record
-      { F₀ = D₀
-      ; unit = now
-      ; extend = _*
-      ; identityʳ = λ {X} {Y} {k} → begin 
-        k * ∘ now ≈⟨ introˡ (IsIso.isoʳ isIso) ⟩∘⟨refl ⟩ 
-        (([ now , later ] ∘ out) ∘ k *) ∘ now ≈⟨ pullʳ *-law ⟩∘⟨refl ⟩
-        ([ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitLaw) ⟩
-        [ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩
-        [ now , later ] ∘ out ∘ k ≈⟨ cancelˡ (IsIso.isoʳ isIso) ⟩
-        k ∎
-      ; identityˡ = λ {X} → sym (*-unique now idC)
-      ; assoc = λ {X} {Y} {Z} {f} {g} → sym (*-unique ((g *) ∘ f) ((g *) ∘ (f *)))
-      ; sym-assoc = λ {X} {Y} {Z} {f} {g} → *-unique ((g *) ∘ f) ((g *) ∘ (f *))
-      ; extend-≈ = *-resp-≈
-      }
+- [ ] Define SearchAlgebras (and SearchAlgebra morphisms)
+- [ ] show StrongEquivalence
+- [ ] Show 'ElgotAlgebra⇔Search+***D***'
+
+
+
  record SearchAlgebras (DF : DelayFunctor) : Set (o ⊔ ℓ ⊔ e) where
+    open DelayFunctor DF
 

\ No newline at end of file
diff --git a/public/index.html b/public/index.html
index 70c379b..a35ad8a 100644
--- a/public/index.html
+++ b/public/index.html
@@ -1 +1,9 @@
-Hello world
\ No newline at end of file
+
+Everything
import ElgotAlgebra
+import ElgotAlgebras
+import Monad.ElgotMonad
+import Monad.Instance.Delay
+import MonadK
+import UniformIterationAlgebra
+import UniformIterationAlgebras
+

\ No newline at end of file
diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md
index fafe8d8..48a4746 100644
--- a/src/Monad/Instance/Delay.lagda.md
+++ b/src/Monad/Instance/Delay.lagda.md
@@ -12,7 +12,9 @@ open import Categories.Object.Terminal
 open import Categories.Category.Construction.F-Coalgebras
 open import Categories.Functor.Coalgebra
 open import Categories.Functor
+open import Categories.Functor.Algebra
 open import Categories.Monad.Construction.Kleisli
+open import Categories.Category.Construction.F-Coalgebras
 import Categories.Morphism as M
 import Categories.Morphism.Reasoning as MR
 ```
@@ -37,20 +39,44 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
   open MR C
   open Equiv
   open HomReasoning
+  open CoLambek
 ```
 ### *Proposition 1*: Characterization of the delay monad ***D***
+
+First I postulate the Functor *D*, maybe I should derive it...
+**TODO**: 
+- how to define using final coalgebra(s)?
+- DX can be defined as retract of infinite streams, how?
+- how to express **Theorem 8** in agda?
+
 ```agda
-  record DelayMonad (D : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
-    open Functor D using () renaming (F₀ to D₀; F₁ to D₁)
+  record DelayFunctor : Set (o ⊔ ℓ ⊔ e) where
+    field
+      D : Endofunctor C
+
+    open Functor D public renaming (F₀ to D₀; F₁ to D₁)
 
     field
       now : ∀ {X} → X ⇒ D₀ X
       later : ∀ {X} → D₀ X ⇒ D₀ X
       isIso : ∀ {X} → IsIso [ now {X} , later {X} ]
-    
+
     out : ∀ {X} → D₀ X ⇒ X + D₀ X
     out {X} = IsIso.inv (isIso {X})
 
+    field
+      coit : ∀ {X Y} → Y ⇒ X + Y → Y ⇒ D₀ X
+      coit-law : ∀ {X Y} {f : Y ⇒ X + Y} → out ∘ (coit f) ≈ (idC +₁ (coit f)) ∘ f
+```
+
+Now let's define the monad:
+
+```agda
+  record DelayMonad : Set (o ⊔ ℓ ⊔ e) where
+    field
+      D : DelayFunctor
+    open DelayFunctor D
+
     field
       _* : ∀ {X Y} → X ⇒ D₀ Y → D₀ X ⇒ D₀ Y
       *-law : ∀ {X Y} {f : X ⇒ D₀ Y} → out ∘ (f *) ≈ [ out ∘ f , i₂ ∘ (f *) ] ∘ out
@@ -81,3 +107,32 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
       ; extend-≈ = *-resp-≈
       }
 ```
+
+### Definition 30: Search-Algebras
+
+```agda
+  record SearchAlgebra (DF : DelayFunctor) : Set (o ⊔ ℓ ⊔ e) where
+    open DelayFunctor DF
+    
+    field
+      FA : F-Algebra D
+
+    open F-Algebra FA
+
+    field
+      now-id : α ∘ now ≈ idC    
+      later-same : α ∘ later ≈ α
+```
+
+### Proposition 31 : the category of uniform-iteration algebras coincides with the category of search-algebras
+TODOs:
+
+- [ ] Define SearchAlgebras (and SearchAlgebra morphisms)
+- [ ] show StrongEquivalence
+- [ ] Show 'ElgotAlgebra⇔Search+***D***'
+
+
+```agda
+  record SearchAlgebras (DF : DelayFunctor) : Set (o ⊔ ℓ ⊔ e) where
+    open DelayFunctor DF
+```
\ No newline at end of file