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

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