sync

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

@@ -32,6 +32,19 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
   open Equality
   open Setoid using () renaming (Carrier to ∣_∣)
 
+  out : ∀ {A : Set ℓ} → A ⊥ → A ⊎ A ⊥
+  out {A} (now x) = inj₁ x
+  out {A} (later x) = inj₂ (♭ x)
+
+  out-cong : ∀ {A : Setoid ℓ ℓ} {x y : ∣ A ∣ ⊥ } → A [ x ≈ y ] → (A ⊎ₛ A ⊥ₛ) [ out x ∼ out y ]
+  out-cong {A} {now x} {now y} x≈y = cong inj₁ₛ (now-inj x≈y)
+  out-cong {A} {now x} {later y} x≈y = {!   !}
+  out-cong {A} {later x} {now y} x≈y = {!   !}
+  out-cong {A} {later x} {later y} x≈y = {!   !}
+
+  ≡to∼ : ∀ {A : Setoid ℓ ℓ} {a b : ∣ A ∣} → a ≡ b → A [ a ∼ b ]
+  ≡to∼ {A} a≡b rewrite a≡b = ∼-refl A
+
   conflict : ∀ {ℓ''} (X Y : Setoid ℓ ℓ) {Z : Set ℓ''}
     {x : ∣ X ∣} {y : ∣ Y ∣} → (X ⊎ₛ Y) [ inj₁ x ∼ inj₂ y ] → Z
   conflict X Y ()
@@ -40,10 +53,54 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
   iter' {A} {X} f (inj₁ x) = x
   iter' {A} {X} f (inj₂ y) = later (♯ iter' {A} {X} f (f y))
 
-  -- TODO works!!
+  -- TODO provable with drop-inj₁ etc...
+  iter'-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ A ⊥ₛ ⊎ₛ X) {x y : ∣ A ∣ ⊥ ⊎ ∣ X ∣} → (A ⊥ₛ ⊎ₛ X) [ x ∼ y ] → A [ iter' (f ._⟨$⟩_) x ≈ iter' (f ._⟨$⟩_) y ]
+  iter'-cong {A} {X} f {x} {y} x∼y with x in eqa | y in eqb 
+  ...                              | inj₁ a        | inj₁ b     = {!   !}
+  ...                              | inj₁ a        | inj₂ b     = {!   !}
+  ...                              | inj₂ a        | inj₁ b     = {!   !}
+  ...                              | inj₂ a        | inj₂ b     = {!   !}
+
   _# : ∀ {A X : Set ℓ} → (X → A ⊥ ⊎ X) → X → A ⊥
   (f #) x = iter' f (inj₂ x)
 
+  #-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ A ⊥ₛ ⊎ₛ X) {x y : ∣ X ∣} → X [ x ∼ y ] → A [ ((f ._⟨$⟩_) #) x ≈ ((f ._⟨$⟩_) #) y ]
+  #-cong {A} {X} f {x} {y} x∼y = later≈ (♯ iter'-cong f (cong f x∼y))
+
+  iter'-Fix : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {x y : ∣ X ∣} → X [ x ∼ y ] → A [ ((f ._⟨$⟩_)#) x ≈ (iter' (f ._⟨$⟩_)) ((f ._⟨$⟩_) y) ]
+  iter'-Fix {A} {X} {f} {x} {y} x∼y = ≈-trans (#-cong f x∼y) helper
+    where
+    helper : A [ ((f ._⟨$⟩_)#) y ≈ (iter' (f ._⟨$⟩_)) ((f ._⟨$⟩_) y) ]
+    helper with (f ._⟨$⟩_) y in eqa 
+    ...    | inj₁ a = ≈-sym (later-eq (later≈ (♯ ≈-sym (iter'-cong f (≡to∼ {A ⊥ₛ ⊎ₛ X} eqa)))))
+    ...    | inj₂ a = later≈ (♯ ≈-trans helper' (≈-sym (later-eq (later≈ (♯ ≈-refl)))))
+      where
+      helper' : A [ iter' (f ._⟨$⟩_) (f ._⟨$⟩_ y) ≈ later (♯ iter' (f ._⟨$⟩_) ((f ._⟨$⟩_) a)) ]
+      helper' = ≈-trans (iter'-cong f (≡to∼ {A ⊥ₛ ⊎ₛ X} eqa)) (later≈ (♯ ≈-refl))
+
+
+  #-Fix : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {x y : ∣ X ∣} → X [ x ∼ y ] → A [ ((f ._⟨$⟩_) #) x ≈ [ Function.id , (f ._⟨$⟩_) # ] ((f ._⟨$⟩_) y) ] -- [ Function.id , iter {A} {X} (f ._⟨$⟩_) ] ((f ._⟨$⟩_) y) ]
+  #-Fix {A} {X} {f} {x} {y} x∼y = ≈-trans (iter'-Fix {A} {X} {f} x∼y) helper
+    where
+    helper : iter' (f ._⟨$⟩_) (f ._⟨$⟩_ y) ≈ [ Function.id , f ._⟨$⟩_ # ] (f ._⟨$⟩_ y)
+    helper with (f ._⟨$⟩_) y in eqa 
+    ...    | inj₁ a = ≈-refl
+    ...    | inj₂ a = later≈ (♯ ≈-refl)
+
+  mutual
+    iter'-Uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {g : Y ⟶ (A ⊥ₛ ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : ∣ A ∣ ⊥ ⊎ ∣ X ∣} → (A ⊥ₛ ⊎ₛ X) [ x ∼ y ] → A [ iter' (f ._⟨$⟩_) x ≈ iter' (g ._⟨$⟩_) ([ inj₁ , (inj₂ ∘′ (h ._⟨$⟩_)) ] y) ]
+    iter'-Uni {A} {X} {Y} {f} {g} {h} hf≋gh {inj₁ x} {inj₁ y} x∼y = drop-inj₁ x∼y
+    iter'-Uni {A} {X} {Y} {f} {g} {h} hf≋gh {inj₂ x} {inj₂ y} x∼y = later≈ (♯ ≈-trans (iter'-cong f (cong f (drop-inj₂ x∼y))) (≈-trans helper (iter'-cong g (hf≋gh (∼-refl X)))))
+      where
+      helper : iter' (f ._⟨$⟩_) (f ⟨$⟩ y) ≈ iter' (g ._⟨$⟩_) ([ inj₁ , (inj₂ ∘′ (h ._⟨$⟩_)) ] (f ⟨$⟩ y))
+      helper with f ⟨$⟩ y in eqa
+      ...    | inj₁ a = ≈-refl
+      ...    | inj₂ a = later≈ (♯ {!   !})
+      -- ...    | inj₂ a = later≈ (♯ ≈-trans (≈-sym (iter'-Fix {A} {X} {f} (∼-refl X))) (≈-trans (#-Uni {A} {X} {Y} {f} {g} {h} hf≋gh {a} {a} (∼-refl X)) (iter'-Fix {A} {Y} {g} (∼-refl Y))))
+
+    -- #-Uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {g : Y ⟶ (A ⊥ₛ ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : ∣ X ∣} → X [ x ∼ y ] → A [ ((f ._⟨$⟩_)#) x ≈ ((g ._⟨$⟩_)#) (h ⟨$⟩ y) ]
+    -- #-Uni {A} {X} {Y} {f} {g} {h} hf≋gh {x} {y} x∼y = later≈ (♯ ≈-trans (iter'-Uni {A} {X} {Y} {f} {g} {h} hf≋gh {f ._⟨$⟩_ x} {f ._⟨$⟩_ y} (cong f x∼y)) (iter'-cong g (hf≋gh (∼-refl X))))
+
   iter : ∀ {A X : Setoid ℓ ℓ} → (∣ X ∣ → (∣ A ∣ ⊥ ⊎ ∣ X ∣)) → ∣ X ∣ → ∣ A ∣ ⊥
   iter {A} {X} f x with f x 
   ...              | inj₁ a = a
@@ -200,10 +257,10 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
 
   delay-lift' : ∀ {A B : Set ℓ} → (A → B) → A ⊥ → B
   delay-lift' {A} {B} f (now x) = f x
-  delay-lift' {A} {B} f (later x) = {!    !} -- (id + f ∘ out)#b
+  delay-lift' {A} {B} f (later x) = {!   !} -- (id + f ∘ out)#b
 
   delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
-  delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = delay-lift' {∣ A ∣} {∣ ⟦ B ⟧ ∣} (f ._⟨$⟩_) ; cong = {!   !} } ; preserves = {!   !} }
+  delay-lift {A} {B} f = record { h = (B Elgot-Algebra.#) {! ? ∘ out  !} ; preserves = {!   !} }
 
   freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A
   freeAlgebra A = record