notes.txt

------------------------- experiments ---------------------------------------------------------------------------------------------

equ : (Moore (List A) B) ≅ (Moore (List⁺ A) B)
equ = record {
    to = moore-list⁺-inclusion
  ; from = moore-list⁺-ext
  ; to∘from=1 = λ { record { E = E ; d = d ; s = s } → {!   !}  }
  ; from∘to=1 = λ { record { E = E ; d = d ; s = s } → {!   !} }
  }

-- if Ji -| moorify', then P∞ _ ⋉ ≅ KL:
-- Ji x -> y
-- ix -> 𝕃y
-- x -> KLy => KL ≅ L'

  {-
  𝕁⊣𝕃' : (M : Moore A B) → (N : Mealy A B) →  (Mealy⇒ N ({!   !} M)) ≅ (Moore⇒ (moorify N) M)
  𝕁⊣𝕃' M N = let module M = Moore M
                 module N = Mealy N in record
    { to = λ α → let module α = Mealy⇒ α in record
      { hom  = λ { m → {!   !} } -- α.hom x , M.s x
      ; d-eq = λ { g → {!   !} } --(a , e) → cong₂ _,_ (α.d-eq _) {! sym (α.s-eq (a , e))  !} } --λ {(a , e) → cong₂ _,_ (α.d-eq (a , e)) (sym (α.s-eq (a , e)))}
      ; s-eq = {!   !} --λ x → refl
      }
    ; from = λ β → let module β = Moore⇒ β in record
      { hom  = λ n → {!   !} --proj₁ ∘ β.hom --λ x → proj₁ (β.hom x)
      ; d-eq = {!   !} --λ {(a , e) → cong proj₁ (β.d-eq (a , e))}
      ; s-eq = {!   !} --λ {(a , e) → trans (sym (cong proj₂ (β.d-eq (a , e)))) (β.s-eq (β.X.d (a , e)))}
      }
    ; to∘from=1 = λ x → let module x = Moore⇒ x
                         in Moore⇒-≡ _ x {!   !} --λ x → let module x = Moore⇒ x
                    --        in Moore⇒-≡ _ x (extensionality (λ t → sym (cong (λ b → proj₁ (x.hom t) , b) (x.s-eq t))))
    ; from∘to=1 = λ x → Mealy⇒-≡ _ x {!   !}
    }
    -}

{-
mealify-advance₂⊣𝕃² : (M : Moore A B) → (N : Mealy A B) → (Mealy⇒ (mealify-advance₂ M) N) ≅ (Moore⇒ M (Queue ⋈ (moorify N)))
mealify-advance₂⊣𝕃² M N = let module M = Moore M
                              module N = Mealy N in
  record { to = λ α → let module α = Mealy⇒ α in
            record { hom = λ {x → ({! α.hom   !} , {!   !}) , {!   !}}
                   ; d-eq = λ {(a , e) → {!  α.s-eq (a , e) !}}
                   ; s-eq = λ x → refl }
         ; from = λ β → let module β = Moore⇒ β in
            record { hom = λ x → {!   !}
                   ; d-eq = λ {(a , e) → {!   !}}
                   ; s-eq = λ {(a , e) → {!   !}} }
         ; to∘from=1 = λ x → let module x = Moore⇒ x in Moore⇒-≡ _ x {!   !}
         ; from∘to=1 = λ x → Mealy⇒-≡ _ x {!   !}
         }

-- can't commute: the number of times one applies moorify must be the same.
-- but:

morphism? : (M : Mealy A B) → Moore⇒ ((moorify ∘ moore-ext ∘ moorify) M)
                                      ((moore-list⁺-ext ∘ moorify ∘ mealy-ext) M)
morphism? M = record
  { hom = λ {((e , b) , b') → e , b'}
  ; d-eq = λ {(e , (e' , b) , b') → cong₂ _,_ {!   !} {!   !}}
  ; s-eq = λ {((e , b') , b) → refl}
  }

quadrato : ∀ {M : Moore A B} → Mealy[ toList , id ] (moore-ext M) ≡ mealy-ext (mealify-advance M)
quadrato {M = record { E = E ; d = d ; s = s }} = {!   !}

morphism2? : (M : Moore A B) → Mealy⇒ (e𝕁 M) (𝕁𝕃e M)
morphism2? M = let module M = Moore M in record
  { hom = λ x → x , M.s x
  ; d-eq = λ {(a ∷ [] , e) → refl
            ; (a ∷ x ∷ as , e) → {!   !} } --cong₂ _,_ (cong (λ t → M.d (a , t)) (cong (λ p → M.d (x , p)) {!   !})) (cong (λ t → M.s (M.d (a , t))) {!   !})}
  ; s-eq = λ {(a ∷ as , e) → {!   !}}
  }

  mealify-advanceₙ : ℕ → Moore A B → Mealy A B
  mealify-advanceₙ {A} {B} n M = record
    { E = Vec B n × M.E
    ; d = λ { (a , f) → {!   !} }
    ; s = λ { (a , g) → M.s {!   !} }
    } where module M = Moore M
            d = flip (curry M.d)

  aggiunzia-divina : ∀ {n}
    → (Mealy⇒ (mealify-advanceₙ n Mre) Mly) ≅ (Moore⇒ Mre (Queueₙ n ⋉ Mly))
  aggiunzia-divina {Mre = Mre} {Mly = Mly} = record
      { to = λ α → let module α = Mealy⇒ α in record
        { hom = λ x → α.hom (replicate (Mre.s x) , x) , replicate (Mre.s x) --α.hom {! Mly.s  !} , replicate (Mre.s x) --λ s → (α.hom (s , {!   !})) , replicate (Mre.s s)
        ; d-eq = {!   !}
        ; s-eq = {!   !}
        }
      ; from = λ α → let module α = Moore⇒ α in record
        { hom = λ f → proj₁ (α.hom (proj₂ f)) --proj₁ (α.hom {! Mre.s  !}) --proj₁ (α.hom (f {! Mre.s  !})) --λ { (s , v) → proj₁ (α.hom s) }
        ; d-eq = {!   !}
        ; s-eq = {!   !}
        }
      ; to∘from=1 = λ x → let module x = Moore⇒ x in
          Moore⇒-≡ _ x (extensionality λ x → {! x.s-eq x  !})
      ; from∘to=1 = λ x → let module x = Mealy⇒ x in
          Mealy⇒-≡ _ x ((extensionality λ x → {! x.d-eq  !}))
      }
    where module Mre = Moore Mre
          module Mly = Mealy Mly

  aggiunzia-divina-reverse : ∀ {n}
    → (Mealy⇒ Mly (mealify-advanceₙ n Mre)) ≅ (Moore⇒ (Queueₙ n ⋉ Mly) Mre)
  aggiunzia-divina-reverse {Mly = Mly} {Mre = Mre} = record
      { to = λ α → let module α = Mealy⇒ α in record
        { hom = {!   !} --λ { (s , x ∷ v) → {! α.hom  !} } --α.hom s {! Mre.s  !} } -- λ s → (α.hom (s , {!   !})) , replicate (Mre.s s)
        ; d-eq = {!   !}
        ; s-eq = {!   !}
        }
      ; from = λ α → let module α = Moore⇒ α in record
        { hom = λ x → {!   !} --replicate (α.hom (x , {! Mre.s  !})) --λ v → α.hom (x , {! Mre.s  !}) --α.hom (x , replicate (Mre.s (Mre.d ({! Mly.d  !} , α.hom {!   !})))) , {!   !} --λ { (s , v) → proj₁ (α.hom s) }
        ; d-eq = {!   !}
        ; s-eq = {!   !}
        }
      ; to∘from=1 = λ x → let module x = Moore⇒ x in
          Moore⇒-≡ _ x (extensionality λ x → {! x.d-eq ?  !})
      ; from∘to=1 = {!   !}
      }
    where module Mre = Moore Mre
          module Mly = Mealy Mly
-}