```{-# 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 WWFoldCommon

(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 FoldTheorems
open FoldTheorems ext fix Computation Induction fix-⊗ FixpointInduction F fmap' fmap-id fmap-comp μ inn out innSur outInj lemma-fold-inn public

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

AssA : Set
AssA = abs ∙ rep ≡ identity

AssB : Set
AssB = abs ∙ rep ∙ f ≡ f

AssC : Set
AssC = fold (abs ∙ rep ∙ f) ≡ fold f

Cond1α : Set
Cond1α = g ≡ rep ∙ f ∙ fmap abs

Cond1β : Set
Cond1β = fold g ≡ fold (rep ∙ f ∙ fmap abs)

Cond2α : Set
Cond2α = (rep ∙ f ≡ g ∙ fmap rep) × Strict rep

Cond2β : Set
Cond2β = fold g ≡ rep ∙ fold f

Cond3α : Set
Cond3α = abs ∙ g ≡ f ∙ fmap abs

WWFactorisation : Set
WWFactorisation = fold f ≡ abs ∙ fold g

WWFusion : Set
WWFusion = rep ∙ abs ∙ fold g ≡ fold g

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

A⇒B : AssA → AssB
A⇒B A =  abs ∙ rep ∙ f
⟨ ∙-assocRL abs rep f ⟩
(abs ∙ rep) ∙ f
⟨ ∙-congR f A ⟩
identity ∙ f
⟨ ∙-idL f ⟩
f
QED

B⇒C : AssB → AssC
B⇒C B = cong fold B

A⇒C : AssA → AssC
A⇒C = B⇒C ∘ A⇒B

1α⇒1β : Cond1α → Cond1β
1α⇒1β α = cong fold α

1αB⇒3α : AssB → Cond1α → Cond3α
1αB⇒3α B =
g ≡ rep ∙ f ∙ fmap abs
→⟨ ∙-congL abs ⟩
abs ∙ g ≡ abs ∙ rep ∙ f ∙ fmap abs
→⟨ ↔-≡ refl (  abs ∙ rep ∙ f ∙ fmap abs
⟨ ∙-assocRRLR abs rep f (fmap abs) ⟩
(abs ∙ rep ∙ f) ∙ fmap abs
⟨ ∙-congR (fmap abs) B ⟩
f ∙ fmap abs
QED )
⟩↔
abs ∙ g ≡ f ∙ fmap abs
Qed

1αA⇒2α : AssA → Strict rep → Cond1α → Cond2α
1αA⇒2α A sr =

g ≡ rep ∙ f ∙ fmap abs
→⟨ ∙-congR (fmap rep) ⟩
g ∙ fmap rep ≡ (rep ∙ f ∙ fmap abs) ∙ fmap rep
→⟨ ↔-≡ refl ( (rep ∙ f ∙ fmap abs) ∙ fmap rep
⟨ ∙-assocLRE rep f (fmap abs) (fmap rep) ⟩
(rep ∙ f) ∙ fmap abs ∙ fmap rep
⟨ ∙-congL (rep ∙ f) ( fmap abs ∙ fmap rep
⟨ sym (fmap-comp abs rep) ⟩
fmap (abs ∙ rep)
⟨ cong fmap A ⟩
fmap identity
⟨ fmap-id ⟩
identity
QED
)
⟩
(rep ∙ f) ∙ identity
⟨ ∙-idR (rep ∙ f) ⟩
rep ∙ f
QED)
⟩↔
g ∙ fmap rep ≡ rep ∙ f
→⟨ (λ eq → sym eq , sr) ⟩
Cond2α
Qed

FactFusionC⇒2β : AssC → WWFactorisation → WWFusion → Cond2β
FactFusionC⇒2β C fact fus =
fold g
⟨ sym fus ⟩
rep ∙ abs ∙ fold g
⟨ ∙-congL rep (sym fact) ⟩
rep ∙ fold f
QED

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