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

module WWFix

(_ : 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))

(A : Type)
(B : Type)

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

where

import FixTheorems
open FixTheorems fix Computation Induction fix-⊗ FixpointInduction

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

AssA : Set
AssA = abs ∙ rep ≡ identity

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

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

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

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

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

Cond2β : Set
Cond2β = fix g ≡ rep \$ fix f

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

WWFactorisation : Set
WWFactorisation = fix f ≡ abs \$ fix g

WWFusion : Set
WWFusion = rep \$ abs \$ fix g ≡ fix g

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

A⇒strictabs : AssA → Strict abs
A⇒strictabs A = ⊑-⊥-eq (ProveTruth (

abs \$ ⊥ ⊑ ⊥
←⟨ ↔-⊑L (
(abs ∙ rep) \$ ⊥
⟨ cong2R _\$_ A ⟩
identity \$ ⊥
⟨ refl ⟩
⊥
QED
)
⟩↔
abs \$ ⊥ ⊑ abs \$ rep \$ ⊥
←⟨ monotonic abs ⟩
⊥ ⊑ rep \$ ⊥
←⟨ ⊑-bot ⟩TRUE
))

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

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 = cong fix

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

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

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

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

fix (rep ∙ f ∙ abs)
⟨ cong fix (∙-assocRL rep f abs) ⟩
fix ((rep ∙ f) ∙ abs)
⟨ RollingRule (rep ∙ f) abs ⟩
(rep ∙ f) \$ fix (abs ∙ rep ∙ f)
⟨ cong (_\$_ (rep ∙ f)) C ⟩
(rep ∙ f) \$ fix f
⟨ cong (_\$_ rep) (sym (Computation f)) ⟩
rep \$ fix f
QED)

1αB⇒3α : AssB → Cond1α → Cond3α
1αB⇒3α B =

g ≡ rep ∙ f ∙ abs
→⟨ ∙-congL abs ⟩
abs ∙ g ≡ abs ∙ rep ∙ f ∙ abs
→⟨ ↔-≡ refl ( abs ∙ rep ∙ f ∙ abs
⟨ ∙-assocRRLR abs rep f abs ⟩
(abs ∙ rep ∙ f) ∙ abs
⟨ ∙-congR abs B ⟩
f ∙ abs
QED
)
⟩↔
abs ∙ g ≡ f ∙ abs
Qed

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

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

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

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

fix f
⟨ sym C ⟩
fix (abs ∙ rep ∙ f)
⟨ RollingRule abs (rep ∙ f) ⟩
abs \$ fix ((rep ∙ f) ∙ abs)
⟨ cong (_\$_ abs ∘ fix) (∙-assocLR rep f abs) ⟩
abs \$ fix (rep ∙ f ∙ abs)
⟨ cong (_\$_ abs) (sym β) ⟩
abs \$ fix 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 \$ fix g
⟨ cong (_\$_ rep) (sym (2βC⇒Fac C β)) ⟩
rep \$ fix f
⟨ sym β ⟩
fix 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β

FactFusionC⇒2β : AssC → WWFactorisation → WWFusion → Cond2β
FactFusionC⇒2β C fact fus =

fix g
⟨ sym fus ⟩
rep \$ abs \$ fix g
⟨ cong (_\$_ rep) (sym fact) ⟩
rep \$ fix f
QED

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

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

3αC⇒Fac : AssC → Cond3α → WWFactorisation
3αC⇒Fac C α = ⊑-antisym leqL leqR
where
leqL : fix f ⊑ abs \$ fix g
leqL = ProveTruth (
fix f ⊑ abs \$ fix g
←⟨ Induction f ⟩
(f ∙ abs) \$ fix g ⊑ abs \$ fix g
←⟨ ↔-⊑R (cong2R _\$_ α) ⟩↔
(abs ∙ g) \$ fix g ⊑ abs \$ fix g
←⟨ ↔-⊑R (cong (_\$_ abs) (Computation g)) ⟩↔
abs \$ fix g  ⊑ abs \$ fix g
←⟨ ⊑-refl ⟩TRUE
)

P : CPO B → Set
P b = abs \$ b ⊑ fix f

ChainCompleteP : ChainComplete P
ChainCompleteP X p =

P (⨆ X)
←⟨ ↔-refl ⟩↔
abs \$ ⨆ X ⊑ fix f
←⟨ ↔-refl ⟩↔
⨆ (chainImage abs X) ⊑ fix f
←⟨ continuity abs X p (fix f) ⟩↔
((b : CPO B) → b ∈ X → abs \$ b ⊑ fix f)
←⟨ ↔-refl ⟩↔
((b : CPO B) → b ∈ X → P b)
Qed

leqR : abs \$ fix g ⊑ fix f
leqR = FixpointInduction P g ChainCompleteP
(ProveTruth (
P ⊥
←⟨ ↔-refl ⟩↔
abs \$ ⊥ ⊑ fix f
←⟨ ↔-⊑L C ⟩↔
abs \$ ⊥ ⊑ fix (abs ∙ rep ∙ f)
←⟨ ↔-⊑L (sym (RollingRule abs (rep ∙ f))) ⟩↔
abs \$ ⊥ ⊑ abs \$ fix ((rep ∙ f) ∙ abs)
←⟨ monotonic abs ⟩
⊥ ⊑ fix ((rep ∙ f) ∙ abs)
←⟨ ⊑-bot ⟩TRUE
)
)
(λ b →
P (g \$ b)
←⟨ ↔-refl ⟩↔
(abs ∙ g) \$ b ⊑ fix f
←⟨ ↔-⊑R (sym (cong2R _\$_ α)) ⟩↔
(f ∙ abs) \$ b ⊑ fix f
←⟨ ↔-⊑L (sym (Computation f)) ⟩↔
f \$ abs \$ b ⊑ f \$ fix f
←⟨ monotonic f ⟩
abs \$ b ⊑ fix f
←⟨ ↔-refl ⟩↔
P b
Qed
)

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

WW-Fix-Fac : AssC → (Cond1α ⊎ Cond1β) ⊎ (Cond2α ⊎ Cond2β) ⊎ Cond3α → WWFactorisation
WW-Fix-Fac C (inl (inl 1α))       = 1αC⇒Fac C 1α
WW-Fix-Fac C (inl (inr 1β))       = 1βC⇒Fac C 1β
WW-Fix-Fac C (inr (inl (inl 2α))) = 2αC⇒Fac C 2α
WW-Fix-Fac C (inr (inl (inr 2β))) = 2βC⇒Fac C 2β
WW-Fix-Fac C (inr (inr 3α))       = 3αC⇒Fac C 3α

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

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