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

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

module WWFoldInstantiate

(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
hiding (RollingRuleFold ; ComputationFold ; FoldFusion ; FoldReflectsStrictness ; FoldFunctorProp)

import FoldTheoremsInstantiated
open FoldTheoremsInstantiated ext fix Computation Induction fix-⊗ FixpointInduction F fmap' fmap-id fmap-comp μ inn out innSur outInj lemma-fold-inn

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

2α⇒2β : Strict f → Cond2α → Cond2β
2α⇒2β sf (β , sr) = sym (FoldFusionInstantiated f g rep sf sr β)

1β⇔2β : Strict abs → Strict rep → Strict f → AssC → Cond1β ↔ Cond2β
1β⇔2β sa sr sf C = ↔-≡ refl (

fold (rep ∙ f ∙ fmap abs)
⟨ cong fold (∙-assocRL rep f (fmap abs)) ⟩
fold ((rep ∙ f) ∙ fmap abs)
⟨ RollingRuleFoldInstantiated (rep ∙ f) (fmap abs) (StrictComposition f rep sf sr) (FmapPreservesStrictness abs sa) ⟩
(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))
⟨ FoldFunctorPropInstantiated
(abs ∙ rep ∙ f)
f
(StrictComposition (rep ∙ f) abs (StrictComposition f rep sf sr) sa)
sf
C
⟩
fold (fmap f)
QED)
⟩
(rep ∙ f) ∙ fold (fmap f)
⟨ ∙-assocLR rep f (fold (fmap f)) ⟩
rep ∙ f ∙ fold (fmap f)
⟨ ∙-congL rep (sym (ComputationFoldInstantiated f sf)) ⟩
rep ∙ fold f
QED
)

1βC⇒Fac : Strict abs → Strict rep → Strict f → AssC → Cond1β → WWFactorisation
1βC⇒Fac sa sr sf C β =

fold f
⟨ sym C ⟩
fold (abs ∙ rep ∙ f)
⟨ RollingRuleFoldInstantiated abs (rep ∙ f) sa (StrictComposition f rep sf sr) ⟩
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 : Strict abs → Strict rep → Strict f → AssC → Cond2β → WWFactorisation
2βC⇒Fac sa sr sf C β = 1βC⇒Fac sa sr sf C (snd (1β⇔2β sa sr sf C) β)

1αC⇒Fac : Strict abs → Strict rep → Strict f → AssC → Cond1α → WWFactorisation
1αC⇒Fac sa sr sf C = 1βC⇒Fac sa sr sf C ∘ 1α⇒1β

2αC⇒Fac : Strict abs → Strict rep → Strict f → AssC → Cond2α → WWFactorisation
2αC⇒Fac sa sr sf C = 2βC⇒Fac sa sr sf C ∘ 2α⇒2β sf

2βC⇒Fusion : Strict abs → Strict rep → Strict f → AssC → Cond2β → WWFusion
2βC⇒Fusion sa sr sf C β =
rep ∙ abs ∙ fold g
⟨ ∙-congL rep (sym (2βC⇒Fac sa sr sf C β)) ⟩
rep ∙ fold f
⟨ sym β ⟩
fold g
QED

1βC⇒Fusion : Strict abs → Strict rep → Strict f → AssC → Cond1β → WWFusion
1βC⇒Fusion sa sr sf C β = 2βC⇒Fusion sa sr sf C (fst (1β⇔2β sa sr sf C) β)

1αC⇒Fusion : Strict abs → Strict rep → Strict f → AssC → Cond1α → WWFusion
1αC⇒Fusion sa sr sf C = 1βC⇒Fusion sa sr sf C ∘ 1α⇒1β

2αC⇒Fusion : Strict abs → Strict rep → Strict f → AssC → Cond2α → WWFusion
2αC⇒Fusion sa sr sf C = 2βC⇒Fusion sa sr sf C ∘ 2α⇒2β sf

FactFusion⇔2β : Strict abs → Strict rep → Strict f → AssC → Cond2β ↔ (WWFactorisation × WWFusion)
FactFusion⇔2β sa sr sf C = (λ β → 2βC⇒Fac sa sr sf C β , 2βC⇒Fusion sa sr sf C β) , uncurry (FactFusionC⇒2β C)

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

3αC⇒Fac : Strict abs → Strict g → AssC → Cond3α → WWFactorisation
3αC⇒Fac sa sg C α = sym (FoldFusionInstantiated g f abs sg sa α)

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

-- Note the many strictness conditions

WW-Fold-Fac : AssC → Strict abs → (((Cond1α ⊎ Cond1β) ⊎ (Cond2α ⊎ Cond2β)) × Strict rep × Strict f) ⊎ (Cond3α × Strict g) → WWFactorisation
WW-Fold-Fac C sa (inl (inl (inl 1α) , sr , sf))  = 1αC⇒Fac sa sr sf C 1α
WW-Fold-Fac C sa (inl (inl (inr 1β) , sr , sf))  = 1βC⇒Fac sa sr sf C 1β
WW-Fold-Fac C sa (inl (inr (inl 2α) , sr , sf))  = 2αC⇒Fac sa sr sf C 2α
WW-Fold-Fac C sa (inl (inr (inr 2β) , sr , sf))  = 2βC⇒Fac sa sr sf C 2β
WW-Fold-Fac C sa (inr (3α , sg))                 = 3αC⇒Fac sa sg C 3α

WW-Fold-Fusion : AssC → Strict abs → Strict rep → Strict f → (Cond1α ⊎ Cond1β) ⊎ (Cond2α ⊎ Cond2β) → WWFusion
WW-Fold-Fusion C sa sr sf (inl (inl 1α)) = 1αC⇒Fusion sa sr sf C 1α
WW-Fold-Fusion C sa sr sf (inl (inr 1β)) = 1βC⇒Fusion sa sr sf C 1β
WW-Fold-Fusion C sa sr sf (inr (inl 2α)) = 2αC⇒Fusion sa sr sf C 2α
WW-Fold-Fusion C sa sr sf (inr (inr 2β)) = 2βC⇒Fusion sa sr sf C 2β

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