From 5f1ab060bb611f57f05835d4d59e41f66b4e7db0 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Thu, 14 Dec 2023 19:11:20 +0100
Subject: [PATCH] Work on example

---
 .../Instance/Setoids/Delay/PreElgot.lagda.md  | 20 +++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md b/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md
index e73b753..54488e7 100644
--- a/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md
@@ -1,7 +1,6 @@
 <!--
 ```agda
 {-# OPTIONS --allow-unsolved-metas --guardedness #-}
-
 open import Level
 open import Relation.Binary
 open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
@@ -66,7 +65,7 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
   ...                                   | 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)))))
-
+  {-# TERMINATING #-}
   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
@@ -88,9 +87,16 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
       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≈ (♯ {!   !})
+  iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₂ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc
+  ...                                                                  | inj₁ c = conflict (delaySetoid A) Y (∼-sym (delaySetoid A ⊎ₛ Y) helper)
+    where
+      helper' : (delaySetoid A ⊎ₛ Y) [ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ∼ g ⟨$⟩ (h ⟨$⟩ y) ]
+      helper' = hf≈gh {x} {y} x∼y
+      helper'' : (delaySetoid A ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ]
+      helper'' rewrite eqx = ∼-refl (delaySetoid A ⊎ₛ Y)
+      helper : (delaySetoid A ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ inj₁ c ]
+      helper rewrite (≡-sym eqc) = ∼-trans (delaySetoid A ⊎ₛ Y) helper'' helper'
+  ...                                                                  | 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)))
   -- 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
@@ -102,9 +108,6 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
       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))
-
 
   -- TODO maybe I can improve inj₁-helper etc. to handle this case as well
   iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (delaySetoid A ⊎ₛ X)) → f ≋ g → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (g ._⟨$⟩_) y ]
@@ -160,6 +163,7 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
 
   -- kleisli lifting (just for making the code cleaner)
   -- TODO
+  -- TODO, freealgebras approach is probably easier
 
   delayPreElgot : IsPreElgot delayMonad
   delayPreElgot = record