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

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