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

open import NeilPrelude hiding (result)
open import Logic
open import Extensionality
open import EquationalEq
open import CPO
open import CPOLemmas
open import CPOFunctions
import Fold

module WWFoldDerived

  (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 ContinuityProps
open ContinuityProps ext fix

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

f' : CPO ((μ F  A)  (μ F  A))
f' = fold-fun f

g' : CPO ((μ F  B)  (μ F  B))
g' = fold-fun g

abs' : CPO ((μ F  B)  (μ F  A))
abs' = result abs

rep' : CPO ((μ F  A)  (μ F  B))
rep' = result rep

import WWFix
open WWFix ext fix Computation Induction fix-⊗ FixpointInduction (μ F  A) (μ F  B) f' g' rep' abs' renaming (AssA to AssA-fix ; AssB to AssB-fix ; AssC to AssC-fix ; Cond1α to Cond1α-fix ; Cond1β to Cond1β-fix ; Cond2α to Cond2α-fix ; Cond2β to Cond2β-fix ; Cond3α to Cond3α-fix ; WWFactorisation to WWFactorisation-fix ; WWFusion to WWFusion-fix)

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

AssA⇒AssA-fix : AssA  AssA-fix
AssA⇒AssA-fix A = cpo-ext  h  abs  rep  h
                                                     ∙-assocRL abs rep h 
                                 (abs  rep)  h
                                                     ∙-congR h A 
                                 identity  h
                                                     ∙-idL h 
                                 h
                                                    QED)

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

AssB⇒AssB-fix : AssB  AssB-fix
AssB⇒AssB-fix B = cpo-ext  h  abs  rep  f  fmap h  out
                                                                ∙-assocRRLR abs rep f (fmap h  out) 
                                 (abs  rep  f)  fmap h  out
                                                                ∙-congR (fmap h  out) B 
                                 f  fmap h  out
                                                               QED )

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

AssC⇔AssC-fix : AssC  AssC-fix
AssC⇔AssC-fix = ↔-≡ (cong fix (cpo-ext  h  (abs  rep  f)  fmap h  out
                                                                              ∙-assocLRRR abs rep f (fmap h  out) 
                                              abs  rep  f  fmap h  out
                                                                             QED)))
                    refl

AssC⇒AssC-fix : AssC  AssC-fix
AssC⇒AssC-fix = fst AssC⇔AssC-fix

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

cond1aux : (h : CPO (μ F  B))  (rep  f  fmap abs)  fmap h  out  rep  f  fmap (abs  h)  out
cond1aux h =
              (rep  f  fmap abs)  fmap h  out
                                                   ∙-assocLR rep (f  fmap abs) (fmap h  out) 
              rep  (f  fmap abs)  fmap h  out
                                                   ∙-congL rep (
                                                                  (f  fmap abs)  fmap h  out
                                                                                                 ∙-assocEC f (fmap abs) (fmap h) out 
                                                                  f  (fmap abs  fmap h)  out
                                                                                                 ∙-congL f (∙-congR out (sym (fmap-comp abs h))) 
                                                                  f  fmap (abs  h)  out
                                                                                                QED )
                                                  
              rep  f  fmap (abs  h)  out
                                                  QED

Cond1α⇒Cond1α-fix : Cond1α  Cond1α-fix
Cond1α⇒Cond1α-fix  = cpo-ext  h   g  fmap h  out
                                                                            ∙-congR (fmap h  out)  
                                       (rep  f  fmap abs)  fmap h  out
                                                                            cond1aux h 
                                       rep  f  fmap (abs  h)  out
                                                                           QED)

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

Cond1β⇔Cond1β-fix : Cond1β  Cond1β-fix
Cond1β⇔Cond1β-fix = ↔-≡ refl (cong fix (cpo-ext cond1aux))

Cond1β⇒Cond1β-fix : Cond1β  Cond1β-fix
Cond1β⇒Cond1β-fix = fst Cond1β⇔Cond1β-fix

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

Cond2α⇒Cond2α-fix : Cond2α  Cond2α-fix
Cond2α⇒Cond2α-fix = 2αAuxEq  fst (PointFreeStrictness rep)
  where
    2αAuxEq : rep  f  g  fmap rep  rep'  f'  g'  rep'
    2αAuxEq  = cpo-ext  h 
                                 rep  f  fmap h  out
                                                                ∙-assocRL rep f (fmap h  out) 
                                 (rep  f)  fmap h  out
                                                                ∙-congR (fmap h  out)  
                                 (g  fmap rep)  fmap h  out
                                                                ∙-assocEC g (fmap rep) (fmap h) out 
                                 g  (fmap rep  fmap h)  out
                                                                ∙-congL g (∙-congR out (sym (fmap-comp rep h))) 
                                 g  fmap (rep  h)  out
                                                               QED)

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

Cond2β⇒Cond2β-fix : Cond2β  Cond2β-fix
Cond2β⇒Cond2β-fix  = 

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

Cond3α⇒Cond3α-fix : Cond3α  Cond3α-fix
Cond3α⇒Cond3α-fix  = cpo-ext  h 

                                 abs  g  fmap h  out
                                                                ∙-assocRL abs g (fmap h  out) 
                                 (abs  g)  fmap h  out
                                                                ∙-congR (fmap h  out)  
                                 (f  fmap abs)  fmap h  out
                                                                ∙-assocEC f (fmap abs) (fmap h) out 
                                 f  (fmap abs  fmap h)  out
                                                                ∙-congL f (∙-congR out (sym (fmap-comp abs h))) 
                                 f  fmap (abs  h)  out
                                                               QED)

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

WWFac-Fix⇒WWFac : WWFactorisation-fix  WWFactorisation
WWFac-Fix⇒WWFac fac = fac

WWFusion-Fix⇒WWFusion : WWFusion-fix  WWFusion
WWFusion-Fix⇒WWFusion fus = fus

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

WW-Fold-Fac : AssC  (Cond1α  Cond1β)  (Cond2α  Cond2β)  Cond3α  WWFactorisation
WW-Fold-Fac C cond = WW-Fix-Fac (AssC⇒AssC-fix C) (map-⊎ (map-⊎ Cond1α⇒Cond1α-fix Cond1β⇒Cond1β-fix)
                                                  (map-⊎ (map-⊎ Cond2α⇒Cond2α-fix Cond2β⇒Cond2β-fix)
                                                                Cond3α⇒Cond3α-fix)
                                                  cond)

WW-Fold-Fusion : AssC  (Cond1α  Cond1β)  (Cond2α  Cond2β)  WWFusion
WW-Fold-Fusion C cond = WW-Fix-Fusion (AssC⇒AssC-fix C) (map-⊎ (map-⊎ Cond1α⇒Cond1α-fix Cond1β⇒Cond1β-fix)
                                                               (map-⊎ Cond2α⇒Cond2α-fix Cond2β⇒Cond2β-fix)
                                                        cond)

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