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

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

where

import FoldTheorems
open FoldTheorems ext fix Computation Induction fix-⊗ FixpointInduction F fmap' fmap-id fmap-comp μ inn out innSur outInj lemma-fold-inn
    hiding (RollingRuleFold ; ComputationFold ; FoldFusion ; FoldReflectsStrictness ; FoldFunctorProp)

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

FoldFusionInstantiated : {σ τ : Type}  (f : CPO (F σ  σ))  (g : CPO (F τ  τ))  (h : CPO (σ  τ))  Strict f  Strict h  h  f  g  fmap h  h  fold f  fold g
FoldFusionInstantiated f g h sf sh =

   h  fold f  fold g
                                                          ←⟨ ↔-sym (UniversalPropFold g (h  fold f) (StrictComposition (fold f) h (FoldPreservesStrictness f sf) sh )) ⟩↔
   (h  fold f)  inn  g  fmap (h  fold f)
                                                          ←⟨ ↔-≡ refl (∙-congL g (sym (fmap-comp h (fold f)))) ⟩↔
   (h  fold f)  inn  g  fmap h  fmap (fold f)
                                                          ←⟨ ↔-≡ (∙-assocRL h (fold f) inn) (∙-assocLR g (fmap h) (fmap (fold f))) ⟩↔
   h  (fold f  inn)  (g  fmap h)  fmap (fold f)
                                                          ←⟨ ↔-≡ (∙-congL h (sym (FoldHomo f))) refl ⟩↔
   h  (f  fmap (fold f))  (g  fmap h)  fmap (fold f)
                                                          ←⟨ ↔-≡ (∙-assocLR h f (fmap (fold f))) refl ⟩↔
   (h  f)  fmap (fold f)  (g  fmap h)  fmap (fold f)
                                                          ←⟨ ∙-congR (fmap (fold f)) 
   h  f  g  fmap h
                                                          Qed

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

RollingRuleFoldInstantiated : {σ τ : Type}  (f : CPO (τ  σ))  (g : CPO (F σ  τ))  Strict f  Strict g  fold (f  g)  f  fold (g  fmap f)
RollingRuleFoldInstantiated f g sf sg = sym (FoldFusionInstantiated
                                                     (g  fmap f)
                                                     (f  g)
                                                     f
                                                     (StrictComposition (fmap f) g (FmapPreservesStrictness f sf) sg)
                                                     sf
                                                     (∙-assocRL f g (fmap f))
                                            )

ComputationFoldInstantiated : {τ : Type}  (f : CPO (F τ  τ))  Strict f  fold f  f  fold (fmap f)
ComputationFoldInstantiated f sf =

   fold f
                                 cong fold (sym (∙-idR f))  
   fold (f  identity)
                                 RollingRuleFoldInstantiated f identity sf refl 
   f  fold (identity  fmap f)
                                 ∙-congL f (cong fold (∙-idL (fmap f))) 
   f  fold (fmap f)
                                QED

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

FoldFunctorPropInstantiated : {τ : Type}  (f g : CPO (F τ  τ))  Strict f  Strict g  fold f  fold g   fold (fmap f)  fold (fmap g)
FoldFunctorPropInstantiated f g sf sg eq =

   fold (fmap f)
                         FFPropAux f sf 
   fmap (fold f)  out
                         ∙-congR out (cong fmap eq) 
   fmap (fold g)  out
                         sym (FFPropAux g sg) 
   fold (fmap g)
                        QED

  where
    FFPropAux : {σ : Type}  (h : CPO (F σ  σ))  Strict h  fold (fmap h)  fmap (fold h)  out
    FFPropAux h sh =

       fold (fmap h)
                                               FoldDef (fmap h) 
       fmap h  fmap (fold (fmap h))  out
                                               ∙-assocRL (fmap h) (fmap (fold (fmap h))) out 
       (fmap h  fmap (fold (fmap h)))  out
                                               ∙-congR out (sym (fmap-comp h (fold (fmap h)))) 
       fmap (h  fold (fmap h))  out
                                               ∙-congR out (cong fmap (sym (ComputationFoldInstantiated h sh))) 
       fmap (fold h)  out
                                              QED

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