```{-# OPTIONS --type-in-type #-}

open import NeilPrelude
open import Extensionality
open import Logic
open import EquationalEq
open import CPO
open import CPOLemmas
open import CPOFunctions
import Fold

module WWFoldDirect

(ext : Extensionality)

(fix : {τ : Type} → CPO (τ ⇒ τ) → CPO τ)
(Computation : {τ : Type} → (f : CPO (τ ⇒ τ)) → fix f ≡ f \$ (fix f))
(Induction : {τ : Type} → {x : CPO τ}  → (f : CPO (τ ⇒ τ)) → f \$ x ⊑ x → fix f ⊑ x)

(fix-⊗ : {σ τ : Type} → {f : CPO (σ ⇒ σ)} → {g : CPO (τ ⇒ τ)} → fix (f :×: g) ≡ (fix f , fix g))

(FixpointInduction : {τ : Type} → (P : CPO τ → Set) → (f : CPO (τ ⇒ τ)) → ChainComplete P → P ⊥ → ((x : CPO τ) → P x → P (f \$ x)) → P (fix f))

(F : Functor)
(fmap' : {σ τ : Type} → CPO ((σ ⇒ τ) ⇒ (F σ ⇒ F τ)))
(fmap-id   : {τ : Type} → fmap' \$ identity {τ} ≡ identity)
(fmap-comp : {σ τ υ : Type} → (f : CPO (τ ⇒ υ)) → (g : CPO (σ ⇒ τ)) → fmap' \$ (f ∙ g) ≡ (fmap' \$ f) ∙ (fmap' \$ g))

(μ : Functor → Type)
(inn    : CPO (F (μ F) ⇒ μ F))
(out    : CPO (μ F ⇒ F (μ F)))
(innSur : inn ∙ out ≡ identity)
(outInj : out ∙ inn ≡ identity)
(lemma-fold-inn : (Fold.fold ext fix F fmap' μ out) inn ≡ identity)

(A : Type)
(B : Type)

(f   : CPO (F A ⇒ A))
(g   : CPO (F B ⇒ B))
(rep : CPO (A ⇒ B))
(abs : CPO (B ⇒ A))

where

import WWFoldCommon
open WWFoldCommon ext fix Computation Induction fix-⊗ FixpointInduction F fmap' fmap-id fmap-comp μ inn out innSur outInj lemma-fold-inn A B f g rep abs

------------------------------------------------

2α⇒2β : Cond2α → Cond2β
2α⇒2β (β , strictrep) = sym (FoldFusion f g rep strictrep β)

1β⇔2β : AssC → Cond1β ↔ Cond2β
1β⇔2β C = ↔-≡ refl (

fold (rep ∙ f ∙ fmap abs)
⟨ cong fold (∙-assocRL rep f (fmap abs)) ⟩
fold ((rep ∙ f) ∙ fmap abs)
⟨ RollingRuleFold (rep ∙ f) (fmap abs) ⟩
(rep ∙ f) ∙ fold (fmap abs ∙ fmap (rep ∙ f))
⟨ ∙-congL (rep ∙ f) (
fold (fmap abs ∙ fmap (rep ∙ f))
⟨ cong fold (sym (fmap-comp abs (rep ∙ f))) ⟩
fold (fmap (abs ∙ rep ∙ f))
⟨ FoldFunctorProp (abs ∙ rep ∙ f) f C ⟩
fold (fmap f)
QED)
⟩
(rep ∙ f) ∙ fold (fmap f)
⟨ ∙-assocLR rep f (fold (fmap f)) ⟩
rep ∙ f ∙ fold (fmap f)
⟨ ∙-congL rep (sym (ComputationFold f)) ⟩
rep ∙ fold f
QED
)

1βC⇒Fac : AssC → Cond1β → WWFactorisation
1βC⇒Fac C β =

fold f
⟨ sym C ⟩
fold (abs ∙ rep ∙ f)
⟨ RollingRuleFold abs (rep ∙ f) ⟩
abs ∙ fold ((rep ∙ f) ∙ fmap abs)
⟨ ∙-congL abs (
fold ((rep ∙ f) ∙ fmap abs)
⟨ cong fold (∙-assocLR rep f (fmap abs)) ⟩
fold (rep ∙ f ∙ fmap abs)
⟨ sym β ⟩
fold g
QED
)
⟩
abs ∙ fold g
QED

2βC⇒Fac : AssC → Cond2β → WWFactorisation
2βC⇒Fac C β = 1βC⇒Fac C (snd (1β⇔2β C) β)

1αC⇒Fac : AssC → Cond1α → WWFactorisation
1αC⇒Fac C = 1βC⇒Fac C ∘ 1α⇒1β

2αC⇒Fac : AssC → Cond2α → WWFactorisation
2αC⇒Fac C = 2βC⇒Fac C ∘ 2α⇒2β

2βC⇒Fusion : AssC → Cond2β → WWFusion
2βC⇒Fusion C β =

rep ∙ abs ∙ fold g
⟨ ∙-congL rep (sym (2βC⇒Fac C β)) ⟩
rep ∙ fold f
⟨ sym β ⟩
fold g
QED

1βC⇒Fusion : AssC → Cond1β → WWFusion
1βC⇒Fusion C β = 2βC⇒Fusion C (fst (1β⇔2β C) β)

1αC⇒Fusion : AssC → Cond1α → WWFusion
1αC⇒Fusion C = 1βC⇒Fusion C ∘ 1α⇒1β

2αC⇒Fusion : AssC → Cond2α → WWFusion
2αC⇒Fusion C = 2βC⇒Fusion C ∘ 2α⇒2β

FactFusion⇔2β : AssC → Cond2β ↔ (WWFactorisation × WWFusion)
FactFusion⇔2β C = (λ β → 2βC⇒Fac C β , 2βC⇒Fusion C β) , uncurry (FactFusionC⇒2β C)

------------------------------------------------

-- Using FoldFusion requires Strict abs
3αC⇒Fac : Strict abs → AssC → Cond3α → WWFactorisation
3αC⇒Fac strictabs C α = sym (FoldFusion g f abs strictabs α)

------------------------------------------------

-- Note the strictness condition
WW-Fold-Fac : AssC → (Cond1α ⊎ Cond1β) ⊎ (Cond2α ⊎ Cond2β) ⊎ (Cond3α × Strict abs) → WWFactorisation
WW-Fold-Fac C (inl (inl 1α))               = 1αC⇒Fac C 1α
WW-Fold-Fac C (inl (inr 1β))               = 1βC⇒Fac C 1β
WW-Fold-Fac C (inr (inl (inl 2α)))         = 2αC⇒Fac C 2α
WW-Fold-Fac C (inr (inl (inr 2β)))         = 2βC⇒Fac C 2β
WW-Fold-Fac C (inr (inr (3α , strictabs))) = 3αC⇒Fac strictabs C 3α

WW-Fold-Fusion : AssC → (Cond1α ⊎ Cond1β) ⊎ (Cond2α ⊎ Cond2β) → WWFusion
WW-Fold-Fusion C (inl (inl 1α)) = 1αC⇒Fusion C 1α
WW-Fold-Fusion C (inl (inr 1β)) = 1βC⇒Fusion C 1β
WW-Fold-Fusion C (inr (inl 2α)) = 2αC⇒Fusion C 2α
WW-Fold-Fusion C (inr (inr 2β)) = 2βC⇒Fusion C 2β

------------------------------------------------
```