minor

agda/src/Monad/Instance/Setoids/K'.lagda.md

@@ -33,6 +33,9 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
   open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≡_])
   open eq using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
 
+  ≡→≡ : ∀ {A : Setoid ℓ ℓ} {x y : ∣ A ∣} → x ≡ y → [ A ][ x ≡ y ]
+  ≡→≡ {A} {x} {y} eq rewrite eq = ≡-refl A
+
   iter : ∀ {A X : Setoid ℓ ℓ} → (∣ X ∣ → (Delay ∣ A ∣ ⊎ ∣ X ∣)) → ∣ X ∣ → Delay ∣ A ∣
   iter′ : ∀ {A X : Setoid ℓ ℓ} → (∣ X ∣ → (Delay ∣ A ∣ ⊎ ∣ X ∣)) → ∣ X ∣ → Delay′ ∣ A ∣
   force (iter′ {A} {X} f x) = iter {A} {X} f x
@@ -81,7 +84,6 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
   ...                                   | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
   ...                                   | inj₂ a | inj₂ b = ≈-trans A (≈-sym A later-self) (iter-cong f (inj₂-helper f x≡y eqx eqy))
 
-
   iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (g ._⟨$⟩_) y ]
   iter-resp-≈′ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈′ iter {A} {X} (g ._⟨$⟩_) y ]
   force≈ (iter-resp-≈′ {A} {X} f g f≋g {x} {y} x≡y) = iter-resp-≈ f g f≋g x≡y
@@ -103,6 +105,26 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
       helper : [ Delayₛ A ⊎ₛ X ][ inj₂ a ≡ inj₂ b ]
       helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y
 
+  iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {g : Y ⟶ (Delayₛ A ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ]
+  iter-uni′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {g : Y ⟶ (Delayₛ A ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈′ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ]
+  force≈ (iter-uni′ {A} {X} {Y} {f} {g} {h} eq {x} {y} x≡y) = iter-uni {A} {X} {Y} {f} {g} {h} eq {x} {y} x≡y
+  iter-uni {A} {X} {Y} {f} {g} {h} eq {x} {y} x≡y with f ⟨$⟩ x in eqx | g ⟨$⟩ (h ⟨$⟩ y) in eqy 
+  ...                                                | inj₁ a         | inj₁ b                 = drop-inj₁ helper
+    where
+      helper' : [ Delayₛ A ⊎ₛ Y ][ [ inj₁ , inj₂ ∘′ < h > ] (f ⟨$⟩ x) ≡ g ⟨$⟩ (h ⟨$⟩ y) ]
+      helper' = eq x≡y
+      helper'' : [ Delayₛ A ⊎ₛ Y ][ inj₁ a ≡ [ inj₁ , inj₂ ∘′ < h > ] (f ⟨$⟩ x) ]
+      helper'' rewrite eqx = ≡-refl (Delayₛ A ⊎ₛ Y)
+      helper : [ Delayₛ A ⊎ₛ Y ][ inj₁ a ≡ inj₁ b ]
+      helper = ≡-trans (Delayₛ A ⊎ₛ Y) helper'' (≡-trans (Delayₛ A ⊎ₛ Y) (eq x≡y) (≡→≡ {Delayₛ A ⊎ₛ Y} eqy))
+  ...                                                | inj₁ a         | inj₂ b                 = {!   !}
+  ...                                                | inj₂ a         | inj₁ b                 = {!   !}
+  -- ...                                                | inj₂ a         | inj₂ b                 = ≈-trans A (later≈ (iter-uni′ {A} {X} {Y} {f} {g} {h} eq {a} {a} (≡-refl X))) (later≈ (iter-cong′ g helper))
+  ...                                                | inj₂ a         | inj₂ b                 = later≈ {!   !}
+    where
+      helper : [ Y ][ h ⟨$⟩ a ≡ b ]
+      helper = {!   !}
+
   iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ X ⊎ₛ Y ∣} → [ X ⊎ₛ Y ][ x ≡ y ] → [ A ][ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} (f ._⟨$⟩_) , inj₂ ∘f (h ._⟨$⟩_) ] x ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f (f ._⟨$⟩_) , (inj₂ ∘f (h ._⟨$⟩_)) ] y ]
   iter-folding′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ X ⊎ₛ Y ∣} → [ X ⊎ₛ Y ][ x ≡ y ] → [ A ][ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} (f ._⟨$⟩_) , inj₂ ∘f (h ._⟨$⟩_) ] x ≈′ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f (f ._⟨$⟩_) , (inj₂ ∘f (h ._⟨$⟩_)) ] y ]
   force≈ (iter-folding′ {A} {X} {Y} {f} {h} {x} {y} x≡y) = iter-folding {A} {X} {Y} {f} {h} x≡y
@@ -146,7 +168,7 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
   open Elgot-Algebra using () renaming (A to ⟦_⟧)
 
   delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
-  delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = ((B Elgot-Algebra.#) helper) ._⟨$⟩_ ; cong = λ {x} {y} x≈y → {!   !} } ; preserves = {!   !} }
+  delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = < (B Elgot-Algebra.#) helper > ; cong = λ {x} {y} x≈y → {!   !} } ; preserves = {!   !} }
     where
     -- (f + id) ∘ out
     helper₁ : Delay ∣ A ∣ → ∣ ⟦ B ⟧ ∣ ⊎ Delay ∣ A ∣
@@ -161,7 +183,7 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
     { FX = delay-algebras A
     ; η = ηₛ A
     ; _* = delay-lift 
-    ; *-lift = {!   !} 
+    ; *-lift = λ {B} f {x} {y} x≡y → ≡-trans ⟦ B ⟧ (Elgot-Algebra.#-Fixpoint B (now∼ x≡y)) (≡-refl ⟦ B ⟧) 
-    ; *-uniq = {!   !} 
+    ; *-uniq = λ {B} f g eq {x} {y} x≡y → {!  !} -- TODO pattern match x and y
     }
 ```