Work on delay monad

agda/src/Category/Ambient/Setoids.lagda.md

@@ -26,8 +26,9 @@ open Eq using (_≡_)
 Most of the required properties are already proven in the agda-categories library, we are only left to construct the natural numbers object.
 
 ```agda
-module Category.Ambient.Setoid {ℓ} where
+module Category.Ambient.Setoids {ℓ} where
   -- equality on setoid functions
+  private
     _≋_ : ∀ {A B : Setoid ℓ ℓ} → A ⟶ B → A ⟶ B → Set ℓ
     _≋_ {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
     ≋-sym : ∀ {A B : Setoid ℓ ℓ} {f g : A ⟶ B} → f ≋ g → g ≋ f

agda/src/Monad/Instance/K/Instance/Delay.lagda.md

@@ -25,6 +25,8 @@ open Eq using (_≡_)
 open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
 open import Codata.Musical.Notation
 import Category.Monad.Partiality
+
+open import Category.Ambient.Setoids
 ```
 -->
 
@@ -105,6 +107,11 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
   now-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Setoid.Carrier A} → A [ x ∼ y ] → A [ now x ≈ now y ]
   now-cong {A} {x} {y} x∼y = ↓≈ x∼y (now↓ (∼-refl A)) (now↓ (∼-refl A))
 
+  -- slightly different types than later≈
+  -- TODO remove this is useless
+  later-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay (Setoid.Carrier A)} → A [ x ≈ y ] → A [ later (♯ x) ≈ later (♯ y) ]
+  later-cong {A} {x} {y} x≈y = later≈ (♯ x≈y)
+
   now-inj : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Setoid.Carrier A} → A [ now x ≈ now y ] → A [ x ∼ y ]
   now-inj {A} {x} {y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = ∼-trans A x∼a (∼-trans A a∼b (∼-sym A y∼b))
 
@@ -239,7 +246,6 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
   identityʳ {A} {now x} {y} x≈y = x≈y
   identityʳ {A} {later x} {y} x≈y = x≈y
 
-
   delayMonad : Monad (Setoids c (c ⊔ ℓ))
   delayMonad = record
     { F = record

agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md

@@ -0,0 +1,127 @@
+<!--
+```agda
+{-# OPTIONS --allow-unsolved-metas --guardedness #-}
+
+open import Level
+open import Relation.Binary
+open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
+open import Data.Sum.Function.Setoid
+open import Data.Sum.Relation.Binary.Pointwise
+open import Function.Equality as SΠ renaming (id to idₛ)
+open import Codata.Musical.Notation
+open import Function using () renaming (_∘_ to _∘f_)
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_) renaming (sym to ≡-sym)
+``` 
+-->
+
+# The delay monad on the category of setoids is pre-Elgot
+
+```agda
+module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
+  open import Monad.Instance.K.Instance.Delay {ℓ} {ℓ}
+  open import Category.Ambient.Setoids
+  open import Algebra.Elgot (setoidAmbient {ℓ})
+  open import Monad.PreElgot (setoidAmbient {ℓ})
+  open Equality
+
+  conflict : ∀ {ℓ''} (X Y : Setoid ℓ ℓ) {Z : Set ℓ''}
+    {x : Setoid.Carrier X} {y : Setoid.Carrier Y } → (X ⊎ₛ Y) [ inj₁ x ∼ inj₂ y ] → Z
+  conflict X Y ()
+
+
+  iter : ∀ {A X : Setoid ℓ ℓ} → (Setoid.Carrier X → (Delay (Setoid.Carrier A) ⊎ Setoid.Carrier X)) → Setoid.Carrier X → Delay (Setoid.Carrier A)
+  iter {A} {X} f x with f x 
+  ...              | inj₁ a = a
+  ...              | inj₂ b = later (♯ (iter {A} {X} f b))
+
+  inj₁-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : Setoid.Carrier X} {a b : Setoid.Carrier Y} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₁ b → Y [ a ∼ b ]
+  inj₁-helper {X} {Y} f {x} {y} {a} {b} x∼y fi₁ fi₂ = drop-inj₁ {x = a} {y = b} helper
+    where
+      helper : (Y ⊎ₛ X) [ inj₁ a ∼ inj₁ b ]
+      helper rewrite (≡-sym fi₁) | (≡-sym fi₂) = cong f x∼y
+
+  inj₂-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : Setoid.Carrier X} {a b : Setoid.Carrier X} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₂ a → f ⟨$⟩ y ≡ inj₂ b → X [ a ∼ b ]
+  inj₂-helper {X} {Y} f {x} {y} {a} {b} x∼y fi₁ fi₂ = drop-inj₂ {x = a} {y = b} helper
+    where
+      helper : (Y ⊎ₛ X) [ inj₂ a ∼ inj₂ b ]
+      helper rewrite (≡-sym fi₁) | (≡-sym fi₂) = cong f x∼y
+
+  absurd-helper : ∀ {ℓ'} {X Y : Setoid ℓ ℓ} {A : Set ℓ'} (f : X ⟶ Y ⊎ₛ X) {x y : Setoid.Carrier X} {a : Setoid.Carrier Y} {b : Setoid.Carrier X} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₂ b → A
+  absurd-helper {ℓ'} {X} {Y} {A} f {x} {y} {a} {b} x∼y fi₁ fi₂ = conflict Y X helper
+    where
+      helper : (Y ⊎ₛ X) [ inj₁ a ∼ inj₂ b ]
+      helper rewrite (≡-sym fi₁) | (≡-sym fi₂) = cong f x∼y
+
+  iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (delaySetoid A ⊎ₛ X)) {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (f ._⟨$⟩_) y ]
+  iter-cong {A} {X} f {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy 
+  ...                             | inj₁ a | inj₁ b = inj₁-helper f x∼y eqx eqy
+  ...                             | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy
+  ...                             | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx
+  ...                             | inj₂ a | inj₂ b = later≈ (♯ iter-cong {A} {X} f (inj₂-helper f x∼y eqx eqy))
+
+  iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ [ Function.id , iter {A} {X} (f ._⟨$⟩_) ] ((f ._⟨$⟩_) y) ]
+  iter-fixpoint {A} {X} {f} {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy
+  ...                                   | inj₁ a | inj₁ b = inj₁-helper f x∼y eqx eqy
+  ...                                   | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy
+  ...                                   | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx
+  ...                                   | inj₂ a | inj₂ b = ≈-sym (later-eq (later≈ (♯ iter-cong f (∼-sym X (inj₂-helper f x∼y eqx eqy)))))
+
+  iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {g : Y ⟶ (delaySetoid A ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ]
+  iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy
+  ...                                                | inj₁ a | inj₁ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc
+  ...                                                                   | inj₁ c = drop-inj₁ {x = a} {y = c} helper
+    where
+      helper'' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ]
+      helper'' rewrite eqx = ⊎-refl ≈-refl (∼-refl Y)
+      helper' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ]
+      helper' = ∼-trans ((delaySetoid A) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y)
+      helper : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ inj₁ c ]
+      helper rewrite (≡-sym eqc) = helper'
+  ...                                                                   | inj₂ c = conflict (delaySetoid A) Y helper
+    where
+      helper'' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ]
+      helper'' rewrite eqx = ⊎-refl ≈-refl (∼-refl Y)
+      helper' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ]
+      helper' = ∼-trans ((delaySetoid A) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y)
+      helper : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ inj₂ c ]
+      helper rewrite (≡-sym eqc) = helper'
+  iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy
+  iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx
+  iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₂ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc --  = ≈-sym (later-eq (later≈ (♯ {!   !}))) -- (iter-uni {A} {X} {Y} {f} {{!   !}} {h} hf≈gh ((inj₂-helper f x∼y eqx eqy)))
+  ...                                                                  | inj₁ c = {!   !} -- absurd, probably...
+  ...                                                                  | inj₂ c = later≈ (♯ {!   !})
+  -- why does this not terminate??
+  -- | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper)))
+    where
+      helper''' : (delaySetoid A ⊎ₛ Y) [ inj₂ c ∼ g ⟨$⟩ (h ⟨$⟩ y) ]
+      helper''' rewrite eqc = ∼-refl (delaySetoid A ⊎ₛ Y)
+      helper'' : (delaySetoid A ⊎ₛ Y) [ g ⟨$⟩ (h ⟨$⟩ y) ∼ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ]
+      helper'' = ∼-sym (delaySetoid A ⊎ₛ Y) (hf≈gh x∼y)
+      helper' : (delaySetoid A ⊎ₛ Y) [ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ∼ inj₂ (h ⟨$⟩ a) ]
+      helper' rewrite eqx = ∼-refl (delaySetoid A ⊎ₛ Y)
+      helper : Y [ c ∼ h ⟨$⟩ a ]
+      helper = drop-inj₂ {x = c} {y = h ⟨$⟩ a} (∼-trans (delaySetoid A ⊎ₛ Y) helper''' (∼-trans (delaySetoid A ⊎ₛ Y) helper'' helper'))
+      help : A [ later (♯ iter {A} {Y} (g ._⟨$⟩_) (h ⟨$⟩ a)) ≈ later (♯ (iter {A} {Y} (g ._⟨$⟩_) c)) ]
+      help = later≈ (♯ iter-cong g (∼-sym Y helper))
+
+  delay-algebras : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (delaySetoid A)
+  delay-algebras {A} = record
+    { _# = λ {X} f → record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = λ {x} {y} x∼y → iter-cong {A} {X} f {x} {y} x∼y }
+    ; #-Fixpoint = λ {X} {f} → iter-fixpoint {A} {X} {f}
+    ; #-Uniformity = λ {X} {Y} {f} {g} {h} → iter-uni {A} {X} {Y} {f} {g} {h}
+    ; #-Folding = {!   !}
+    ; #-resp-≈ = {!   !}
+    }
+    where
+      iterr : ∀ {X : Setoid ℓ ℓ} → X ⟶ ((delaySetoid A) ⊎ₛ X) → X ⟶ (delaySetoid A)
+      iterr {X} f = record { _⟨$⟩_ = {!   !} ; cong = {!   !} }
+
+  delayPreElgot : IsPreElgot delayMonad
+  delayPreElgot = record 
+    { elgotalgebras = delay-algebras
+    ; extend-preserves = {!   !} 
+    }
+
+
+```