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

open import NeilPrelude
open import Extensionality
open import CPO
open import CPOFunctions

module Fold

  (ex : Extensionality)

  (fix : {τ : Type} → CPO (τ ⇒ τ) → CPO τ)

  (F : Functor)
  (fmap' : {σ τ : Type} → CPO ((σ ⇒ τ) ⇒ (F σ ⇒ F τ)))

  (μ : Functor → Type)
  (out : CPO (μ F ⇒ F (μ F)))

where

import ContinuityProps
open ContinuityProps ex fix

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

-- fold-fun f = (λ h → f ∙ fmap h ∙ out)
fold-fun : {σ τ : Type} → (f : CPO (F σ ⇒ τ)) → CPO ((μ F ⇒ σ) ⇒ μ F ⇒ τ)
fold-fun f = resultArg f out ∙ fmap'

-- fold f = fix (λ h → f ∙ fmap h ∙ out)
fold : {τ : Type} → CPO (F τ ⇒ τ) → CPO (μ F ⇒ τ)
fold f = fix (fold-fun f)

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