leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

continue refactor

Browse source
This commit is contained in:
Leon Vatthauer 2023-12-22 17:54:11 +01:00
parent 395f548334
commit f5ae9924eb
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 158 additions and 195 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
agda/src/Monad/Instance/K/Instance/Delay.lagda.md
View file

@ -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ʳ
}
```

329
agda/src/Monad/Instance/Setoids/K.lagda.md
View file

@ -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,12 +205,37 @@ 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