diff --git a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md index 29a9927..3dde1cb 100644 --- a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md +++ b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md @@ -209,28 +209,17 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where μ-assoc↓ {A} {now x} {y} (now↓ x≈y) = x≈y μ-assoc↓ {A} {later x} {y} (later↓ x↓y) = ≈-sym A (later-eq (later≈ (♯ ≈-sym A (μ-assoc↓ x↓y)))) + -- TODO remove if nowhere needed μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} {z : ∣ A ∣} → [ A ⊥ₛ ][ x ↓ y ] → [ A ][ y ↓ z ] → [ A ][ (μₛ A ⟨$⟩ x) ↓ z ] μ↓-trans {A} {now x} {y} {z} (now↓ x≈y) y↓z = ≈↓ A (≈-sym A x≈y) y↓z μ↓-trans {A} {later x} {y} {z} (later↓ x↓y) y↓z = later↓ (μ↓-trans x↓y y↓z) --- -- μ↓-trans² : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (∣ A ∣ ⊥))} {y : Delay (∣ A ∣ ⊥)} {z : ∣ A ∣ ⊥} → _↓_ {delaySetoid (A ⊥ₛ)} x y → _↓_ {A ⊥ₛ} y z → _↓_ {A ⊥ₛ} ((delayFun (μ A)) ⟨$⟩ x) z --- -- μ↓-trans² {A} {now x} {y} {now x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {! !} (μ↓-trans {! !} {! y↓z !}) (now↓ (∼-refl A))) --- -- μ↓-trans² {A} {now x} {y} {later x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {! !} {! !} {! !}) --- -- μ↓-trans² {A} {later x} {y} {z} x↓y y↓z = {! !} - μ-assoc' : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ((∣ A ∣ ⊥)⊥)⊥} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼ (μₛ A ∘ μₛ (A ⊥ₛ)) ⟨$⟩ x ] μ-assoc' {A} {now x} = ∼-refl A μ-assoc' {A} {later x} = later∼ (♯ μ-assoc' {A} {♭ x}) - -- TODO μ-assoc follows from this!! - --- μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ (delayFun (μ A))) ≋ (μ A ∘ μ (A ⊥ₛ)) --- μ-assoc {A} {now x} {now y} (↓≈ a≈b (now↓ x≈a) (now↓ y≈b)) = cong (μ A) (≈-trans x≈a (≈-trans a≈b (≈-sym y≈b))) --- μ-assoc {A} {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = later-eq (later≈ (♯ cong (μ A) (≈-sym (μ↓ (∼↓ (≈-sym (≈-trans x≈a a≈b)) y↓b))))) -- y , liftF (μ A) (♭ x) --- μ-assoc {A} {later x} {now y} (↓≈ {_} {_} {a} {b} (↓≈ c≈d a↓c b↓d) (later↓ x↓a) (now↓ y≈b)) = ≈-sym (later-eq (later≈ (♯ cong (μ A) {y} {liftF (μ A) (♭ x)} (↓≈ (≈-sym c≈d) (≈↓ (≈-sym y≈b) b↓d) {! delayFun↓ (μ A) {♭ x} x↓a !})))) -- (↓≈ (≈-sym c≈d) (≈↓ (≈-sym y≈b) b↓d) (μ↓-trans {! x↓a !} a↓c)) --- μ-assoc {A} {later x} {now y} (↓≈ (later≈ x≈y) (later↓ x↓a) (now↓ y≈b)) = {! !} --- μ-assoc {A} {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ μ-assoc (↓≈ a≈b x↓a y↓b)) --- μ-assoc {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ μ-assoc (♭ x≈y)) + μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ (liftFₛ (μₛ A))) ≋ (μₛ A ∘ μₛ (A ⊥ₛ)) + μ-assoc {A} {x} {y} x≈y = ≈-trans A (μ-cong A (lift-cong (μₛ A) x≈y)) (∼⇒≈ (μ-assoc' {A} {y})) identityˡ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ∣ A ∣ ⊥} {y : ∣ A ∣} → [ A ][ x ↓ y ] → [ A ][ ((μₛ A) ⟨$⟩ ((liftFₛ (η A)) ⟨$⟩ x)) ↓ y ] identityˡ↓ {A} {now x} {y} x↓y = x↓y @@ -257,10 +246,9 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where } ; η = ntHelper (record { η = η ; commute = η-natural }) ; μ = ntHelper (record { η = μₛ ; commute = μ-natural }) - ; assoc = {! !} - ; sym-assoc = {! !} + ; assoc = μ-assoc + ; sym-assoc = λ {A} {x} {y} x≈y → ≈-sym A (μ-assoc (≈-sym ((A ⊥ₛ) ⊥ₛ) x≈y)) ; identityˡ = identityˡ ; identityʳ = identityʳ } - ``` \ No newline at end of file diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md index c2167a1..22c3cbc 100644 --- a/agda/src/Monad/Instance/Setoids/K.lagda.md +++ b/agda/src/Monad/Instance/Setoids/K.lagda.md @@ -10,7 +10,7 @@ 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) +open Eq using (_≡_) renaming (sym to ≣-sym) open import FreeObject open import Categories.FreeObjects.Free open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) @@ -29,221 +29,171 @@ module Monad.Instance.Setoids.K {ℓ : Level} where open import Algebra.Elgot.Free (setoidAmbient {ℓ}) open import Category.Construction.ElgotAlgebras (setoidAmbient {ℓ}) open import Monad.PreElgot (setoidAmbient {ℓ}) - open Equality - open Setoid using () renaming (Carrier to ∣_∣) + open WeakBisimilarity renaming (_≈_ to [_][_≈_]) + open StrongBisimilarity renaming (_∼_ to [_][_∼_]) + open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≡_]) + open eq using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans) - 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 + ≡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 + {x : ∣ X ∣} {y : ∣ Y ∣} → [ X ⊎ₛ Y ][ inj₁ x ≡ inj₂ y ] → Z conflict X Y () - - iter' : ∀ {A X : Set ℓ} → (X → A ⊥ ⊎ X) → A ⊥ ⊎ X → A ⊥ - iter' {A} {X} f (inj₁ x) = x - iter' {A} {X} f (inj₂ y) = later (♯ iter' {A} {X} f (f y)) - - -- 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 ... | inj₂ b = later (♯ (iter {A} {X} f b)) - inj₁-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a b : ∣ 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 + inj₁-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a b : ∣ 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 + 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 : ∣ X ∣} {a b : ∣ 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 + inj₂-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a b : ∣ 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 + 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 : ∣ X ∣} {a : ∣ Y ∣} {b : ∣ 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 + absurd-helper : ∀ {ℓ'} {X Y : Setoid ℓ ℓ} {A : Set ℓ'} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a : ∣ Y ∣} {b : ∣ 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 + helper : [ Y ⊎ₛ X ][ inj₁ a ≡ inj₂ b ] + helper rewrite (≣-sym fi₁) | (≣-sym fi₂) = cong f x≡y - iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (A ⊥ₛ ⊎ₛ X)) {x y : ∣ 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-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (A ⊥ₛ ⊎ₛ X)) {x y : ∣ 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 ⟶ (A ⊥ₛ ⊎ₛ X)} {x y : ∣ 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-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {x y : ∣ 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 A (later-eq (later≈ (♯ iter-cong f (≡-sym X (inj₂-helper f x≡y eqx eqy))))) iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (A ⊥ₛ ⊎ₛ X)) → X ⟶ A ⊥ₛ iterₛ {A} {X} f = record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = iter-cong {A} {X} f } - -- 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 : ∣ 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 = ≈-trans (helper x) (iter-cong g (cong h x∼y)) + iter-uni' : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {g : Y ⟶ (A ⊥ₛ ⊎ₛ Y)} {h : X ⟶ Y} → (∀ {x y : ∣ X ∣} → [ A ⊥ₛ ⊎ₛ Y ][ ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ⟨$⟩ x ≡ (g ∘ h) ⟨$⟩ y ]) → ∀ {x y : ∣ 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 = {! !} + + 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 : ∣ 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 = ≈-trans A (≈-trans A (≈-trans A (iter-cong f x≡y) {! !}) (cong [ idₛ , iterₛ {A} {Y} g ]ₛ (hf≋gh (≡-refl X)))) (≈-sym A (iter-fixpoint {A} {Y} {g} {h ⟨$⟩ y} {h ⟨$⟩ y} (≡-refl Y))) + where + helper : [ A ][ iter {A} {X} (f ._⟨$⟩_) y ≈ ([ [ Function.id , iter {A} {Y} (g ._⟨$⟩_) ] ∘′ inj₁ , [ Function.id , iter {A} {Y} (g ._⟨$⟩_) ] ∘′ inj₂ ∘′ (h ._⟨$⟩_) ] (f ⟨$⟩ y))] + helper with f ⟨$⟩ y in eqa + ... | inj₁ a = ≈-refl A + ... | inj₂ a = ≈-sym A (later-eq (later≈ (♯ {! !}))) + -- helper : [ A ][ iter (f ._⟨$⟩_) y ≈ [ Function.id , iter {A} {Y} (g ._⟨$⟩_) ] ([ inj₁ , inj₂ ∘′ (h ._⟨$⟩_) ] (f ⟨$⟩ y))] + -- helper with f ⟨$⟩ y in eqa + -- ... | inj₁ a = {! !} + -- ... | inj₂ a = {! !} + -- iter-uni' {A} {X} {Y} {f} {g} {h} hf≋gh {x} {y} x≡y with f ⟨$⟩ x in eqa | g ⟨$⟩ (h ⟨$⟩ y) in eqb + -- ... | inj₁ a | inj₁ b = {! !} + -- ... | inj₁ a | inj₂ b = {! !} -- absurd + -- ... | inj₂ a | inj₁ b = {! !} -- absurd + -- ... | inj₂ a | inj₂ b = later∼ (♯ {! !}) + + -- {-# TERMINATING #-} + -- 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 : ∣ 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 : ∀ (x : ∣ X ∣) → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ x) ] - -- helper x with f ⟨$⟩ x in eqa | g ⟨$⟩ (h ⟨$⟩ x) in eqb - -- ... | inj₁ a | inj₁ b = {! !} - -- ... | inj₁ a | inj₂ b = {! !} -- absurd - -- ... | inj₂ a | inj₁ b = {! !} -- absurd - -- ... | inj₂ a | inj₂ b rewrite (≡-sym eqb) = {! !} -- later≈ (♯ {! iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {a} {(h ⟨$⟩ a)} !}) -- ≈-trans {_} {{! !}} (later≈ {{! !}} {{! !}} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ helper a)) (later≈ (♯ {! !})) + -- helper'' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ≡ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ] + -- helper'' rewrite eqx = ⊎-refl ≈-refl (≡-refl Y) + -- helper' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ≡ (g ⟨$⟩ (h ⟨$⟩ y)) ] + -- helper' = ≡-trans ((A ⊥ₛ) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x≡y) + -- helper : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ≡ inj₁ c ] + -- helper rewrite (≡-sym eqc) = helper' + -- ... | inj₂ c = conflict (A ⊥ₛ) Y helper + -- where + -- helper'' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ≡ [ inj₁ , (λ lx₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ] + -- helper'' rewrite eqx = ⊎-refl ≈-refl (≡-refl Y) + -- helper' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ≡ (g ⟨$⟩ (h ⟨$⟩ y)) ] + -- helper' = ≡-trans ((A ⊥ₛ) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x≡y) + -- helper : (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 + -- ... | inj₁ c = conflict (A ⊥ₛ) Y (≡-sym (A ⊥ₛ ⊎ₛ Y) helper) + -- where + -- helper' : (A ⊥ₛ ⊎ₛ Y) [ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ≡ g ⟨$⟩ (h ⟨$⟩ y) ] + -- helper' = hf≈gh {x} {y} x≡y + -- helper'' : (A ⊥ₛ ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ≡ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ] + -- helper'' rewrite eqx = ≡-refl (A ⊥ₛ ⊎ₛ Y) + -- helper : (A ⊥ₛ ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ≡ inj₁ c ] + -- helper rewrite (≡-sym eqc) = ≡-trans (A ⊥ₛ ⊎ₛ Y) helper'' helper' + -- ... | inj₂ c = later≈ {! !} -- ≈-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 + -- helper''' : (A ⊥ₛ ⊎ₛ Y) [ inj₂ c ≡ g ⟨$⟩ (h ⟨$⟩ y) ] + -- helper''' rewrite eqc = ≡-refl (A ⊥ₛ ⊎ₛ Y) + -- helper'' : (A ⊥ₛ ⊎ₛ Y) [ g ⟨$⟩ (h ⟨$⟩ y) ≡ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ] + -- helper'' = ≡-sym (A ⊥ₛ ⊎ₛ Y) (hf≈gh x≡y) + -- helper' : (A ⊥ₛ ⊎ₛ Y) [ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ≡ inj₂ (h ⟨$⟩ a) ] + -- helper' rewrite eqx = ≡-refl (A ⊥ₛ ⊎ₛ Y) + -- helper : Y [ c ≡ h ⟨$⟩ a ] + -- helper = drop-inj₂ {x = c} {y = h ⟨$⟩ a} (≡-trans (A ⊥ₛ ⊎ₛ Y) helper''' (≡-trans (A ⊥ₛ ⊎ₛ Y) helper'' helper')) - {-# TERMINATING #-} - 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 : ∣ 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'' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ] - helper'' rewrite eqx = ⊎-refl ≈-refl (∼-refl Y) - helper' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ] - helper' = ∼-trans ((A ⊥ₛ) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y) - helper : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ inj₁ c ] - helper rewrite (≡-sym eqc) = helper' - ... | inj₂ c = conflict (A ⊥ₛ) Y helper - where - helper'' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ] - helper'' rewrite eqx = ⊎-refl ≈-refl (∼-refl Y) - helper' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ] - helper' = ∼-trans ((A ⊥ₛ) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y) - helper : (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 - ... | inj₁ c = conflict (A ⊥ₛ) Y (∼-sym (A ⊥ₛ ⊎ₛ Y) helper) - where - helper' : (A ⊥ₛ ⊎ₛ Y) [ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ∼ g ⟨$⟩ (h ⟨$⟩ y) ] - helper' = hf≈gh {x} {y} x∼y - helper'' : (A ⊥ₛ ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ] - helper'' rewrite eqx = ∼-refl (A ⊥ₛ ⊎ₛ Y) - helper : (A ⊥ₛ ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ inj₁ c ] - helper rewrite (≡-sym eqc) = ∼-trans (A ⊥ₛ ⊎ₛ Y) helper'' helper' - ... | inj₂ c = later≈ {! !} -- ≈-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 - helper''' : (A ⊥ₛ ⊎ₛ Y) [ inj₂ c ∼ g ⟨$⟩ (h ⟨$⟩ y) ] - helper''' rewrite eqc = ∼-refl (A ⊥ₛ ⊎ₛ Y) - helper'' : (A ⊥ₛ ⊎ₛ Y) [ g ⟨$⟩ (h ⟨$⟩ y) ∼ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ] - helper'' = ∼-sym (A ⊥ₛ ⊎ₛ Y) (hf≈gh x∼y) - helper' : (A ⊥ₛ ⊎ₛ Y) [ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ∼ inj₂ (h ⟨$⟩ a) ] - helper' rewrite eqx = ∼-refl (A ⊥ₛ ⊎ₛ Y) - helper : Y [ c ∼ h ⟨$⟩ a ] - helper = drop-inj₂ {x = c} {y = h ⟨$⟩ a} (∼-trans (A ⊥ₛ ⊎ₛ Y) helper''' (∼-trans (A ⊥ₛ ⊎ₛ Y) helper'' helper')) - - -- TODO maybe I can improve inj₁-helper etc. to handle this case as well - iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (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} f g f≋g {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (g ._⟨$⟩_) y in eqy + -- -- TODO maybe I can improve inj₁-helper etc. to handle this case as well + iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (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} f g f≋g {x} {y} x≡y with (f ._⟨$⟩_) x in eqx | (g ._⟨$⟩_) y in eqy ... | inj₁ a | inj₁ b = drop-inj₁ helper where - helper : (A ⊥ₛ ⊎ₛ X) [ inj₁ a ∼ inj₁ b ] - helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y + helper : [ A ⊥ₛ ⊎ₛ X ][ inj₁ a ≡ inj₁ b ] + helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y ... | inj₁ a | inj₂ b = conflict (A ⊥ₛ) X helper where - helper : (A ⊥ₛ ⊎ₛ X) [ inj₁ a ∼ inj₂ b ] - helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y - ... | inj₂ a | inj₁ b = conflict (A ⊥ₛ) X (∼-sym (A ⊥ₛ ⊎ₛ X) helper) + helper : [ A ⊥ₛ ⊎ₛ X ][ inj₁ a ≡ inj₂ b ] + helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y + ... | inj₂ a | inj₁ b = conflict (A ⊥ₛ) X (≡-sym (A ⊥ₛ ⊎ₛ X) helper) where - helper : (A ⊥ₛ ⊎ₛ X) [ inj₂ a ∼ inj₁ b ] - helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y + helper : [ A ⊥ₛ ⊎ₛ X ][ inj₂ a ≡ inj₁ b ] + helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y ... | inj₂ a | inj₂ b = later≈ (♯ iter-resp-≈ {A} {X} f g f≋g (drop-inj₂ helper)) where - helper : (A ⊥ₛ ⊎ₛ X) [ inj₂ a ∼ inj₂ b ] - helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y + helper : [ A ⊥ₛ ⊎ₛ X ][ inj₂ a ≡ inj₂ b ] + helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y - iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (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} {f} {h} {inj₁ x} {inj₁ y} ix∼iy with f ⟨$⟩ x in eqx | f ⟨$⟩ y in eqy - ... | inj₁ a | inj₁ b = inj₁-helper f (drop-inj₁ ix∼iy) eqx eqy - ... | inj₁ a | inj₂ b = absurd-helper f (drop-inj₁ ix∼iy) eqx eqy - ... | inj₂ a | inj₁ b = absurd-helper f (∼-sym X (drop-inj₁ ix∼iy)) eqy eqx - ... | inj₂ a | inj₂ b = later≈ (♯ ≈-trans (iter-cong f (inj₂-helper f (drop-inj₁ ix∼iy) eqx eqy)) (helper b)) + iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (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} {f} {h} {inj₁ x} {inj₁ y} ix≡iy with f ⟨$⟩ x in eqx | f ⟨$⟩ y in eqy + ... | inj₁ a | inj₁ b = inj₁-helper f (drop-inj₁ ix≡iy) eqx eqy + ... | inj₁ a | inj₂ b = absurd-helper f (drop-inj₁ ix≡iy) eqx eqy + ... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X (drop-inj₁ ix≡iy)) eqy eqx + ... | inj₂ a | inj₂ b = later≈ (♯ ≈-trans A (iter-cong f (inj₂-helper f (drop-inj₁ ix≡iy) eqx eqy)) (helper b)) where - helper : ∀ (b : ∣ X ∣) → A [ iter {A} {X} (f ._⟨$⟩_) b ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ (f ._⟨$⟩_) , inj₂ ∘′ (h ._⟨$⟩_) ] (inj₁ b) ] + helper : ∀ (b : ∣ X ∣) → [ A ][ iter {A} {X} (f ._⟨$⟩_) b ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ (f ._⟨$⟩_) , inj₂ ∘′ (h ._⟨$⟩_) ] (inj₁ b) ] helper b with f ⟨$⟩ b in eqb - ... | inj₁ c = ∼-refl (A ⊥ₛ) + ... | inj₁ c = ≡-refl (A ⊥ₛ) ... | inj₂ c = later≈ (♯ helper c) - iter-folding {A} {X} {Y} {f} {h} {inj₂ x} {inj₂ y} ix∼iy with h ⟨$⟩ x in eqx | h ⟨$⟩ y in eqy + iter-folding {A} {X} {Y} {f} {h} {inj₂ x} {inj₂ y} ix≡iy with h ⟨$⟩ x in eqx | h ⟨$⟩ y in eqy ... | inj₁ a | inj₁ b = later≈ (♯ iter-folding {A} {X} {Y} {f} {h} {inj₁ a} {inj₁ b} helper) where - helper : (X ⊎ₛ Y) [ inj₁ a ∼ inj₁ b ] - helper rewrite (≡-sym eqx) | (≡-sym eqy) = cong h (drop-inj₂ ix∼iy) - ... | inj₁ a | inj₂ b = absurd-helper h (drop-inj₂ ix∼iy) eqx eqy - ... | inj₂ a | inj₁ b = absurd-helper h (∼-sym Y (drop-inj₂ ix∼iy)) eqy eqx + helper : [ X ⊎ₛ Y ][ inj₁ a ≡ inj₁ b ] + helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy) + ... | inj₁ a | inj₂ b = absurd-helper h (drop-inj₂ ix≡iy) eqx eqy + ... | inj₂ a | inj₁ b = absurd-helper h (≡-sym Y (drop-inj₂ ix≡iy)) eqy eqx ... | inj₂ a | inj₂ b = later≈ (♯ iter-folding {A} {X} {Y} {f} {h} {inj₂ a} {inj₂ b} helper) where - helper : (X ⊎ₛ Y) [ inj₂ a ∼ inj₂ b ] - helper rewrite (≡-sym eqx) | (≡-sym eqy) = cong h (drop-inj₂ ix∼iy) + helper : [ X ⊎ₛ Y ][ inj₂ a ≡ inj₂ b ] + helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy) delay-algebras-on : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (A ⊥ₛ) delay-algebras-on {A} = record { _# = iterₛ {A} ; #-Fixpoint = λ {X} {f} → iter-fixpoint {A} {X} {f} - ; #-Uniformity = λ {X} {Y} {f} {g} {h} → iter-uni {A} {X} {Y} {f} {g} {h} - ; #-Folding = λ {X} {Y} {f} {h} {x} {y} x∼y → iter-folding {A} {X} {Y} {f} {h} {x} {y} x∼y + ; #-Uniformity = {! !} -- λ {X} {Y} {f} {g} {h} → iter-uni {A} {X} {Y} {f} {g} {h} + ; #-Folding = λ {X} {Y} {f} {h} {x} {y} x≡y → iter-folding {A} {X} {Y} {f} {h} {x} {y} x≡y ; #-resp-≈ = λ {X} {f} {g} → iter-resp-≈ {A} {X} f g } @@ -255,16 +205,41 @@ module Monad.Instance.Setoids.K {ℓ : Level} where nowₛ : ∀ {A : Setoid ℓ ℓ} → A ⟶ A ⊥ₛ nowₛ = record { _⟨$⟩_ = now ; cong = now-cong } - 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 + outₛ : ∀ {A : Setoid ℓ ℓ} → A ⊥ₛ ⟶ A ⊎ₛ A ⊥ₛ + outₛ {A} = record { _⟨$⟩_ = out ; cong = {! !} } + where + out⁻¹ : ∣ A ⊎ₛ A ⊥ₛ ∣ → ∣ A ⊥ₛ ∣ + out⁻¹ = [ now , (λ x → later (♯ x)) ] + out : ∣ A ⊥ₛ ∣ → ∣ A ⊎ₛ A ⊥ₛ ∣ + out (now x) = inj₁ x + out (later x) = inj₂ (♭ x) + out-cong : ∀ {x y : ∣ A ⊥ₛ ∣} → [ A ⊥ₛ ][ x ≡ y ] → [ A ⊎ₛ A ⊥ₛ ][ out x ≡ out y ] + out-cong {now x} {now y} x≡y = {! !} + out-cong {now x} {later y} x≡y = {! !} + out-cong {later x} {now y} x≡y = {! !} + out-cong {later x} {later y} x≡y = {! !} + + lift'' : ∀ {A B : Set ℓ} → (∀ (C : Set ℓ) → (A ⊥ → B ⊎ A ⊥) → A ⊥ → B) → (A → B) → A ⊥ → B + lift'' {A} {B} [_]_# f = [ B ] (λ { (now x) → inj₁ (f x) ; (later x) → inj₂ (later (♯ {! !})) }) # delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B - delay-lift {A} {B} f = record { h = (B Elgot-Algebra.#) {! ? ∘ out !} ; preserves = {! !} } + delay-lift {A} {B} f = record { h = (B Elgot-Algebra.#) helper ; preserves = {! !} } + where + helper₁ : ∣ A ∣ ⊥ → ∣ ⟦ B ⟧ ∣ ⊎ ∣ A ∣ ⊥ + helper₁ (now x) = inj₁ (< f > x) + helper₁ (later x) = inj₂ (♭ x) + helper₁-cong : ∀ {x y : ∣ A ∣ ⊥} → [ A ][ x ≈ y ] → [ ⟦ B ⟧ ⊎ₛ A ⊥ₛ ][ helper₁ x ≡ helper₁ y ] + helper₁-cong {now x} {now y} x≈y = {! !} -- yes + helper₁-cong {now x} {later y} x≈y = {! !} + helper₁-cong {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = {! !} + helper₁-cong {later x} {later y} (later≈ x≈y) = {! !} -- cong inj₂ₛ (♭ x≈y) + helper₁-cong {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = {! !} --cong inj₂ₛ (↓≈ a≡b x↓a y↓b) + helper : A ⊥ₛ ⟶ ⟦ B ⟧ ⊎ₛ A ⊥ₛ + helper = record { _⟨$⟩_ = helper₁ ; cong = helper₁-cong } freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A freeAlgebra A = record - { FX = delay-algebras A + { FX = delay-algebras A ; η = nowₛ {A} ; _* = delay-lift ; *-lift = {! !}