{-# OPTIONS --allow-unsolved-metas #-}

open import Categories.Category
open import Monad.Instance.Delay
open import Categories.Category.Distributive
open import Categories.Object.Terminal 
open import Categories.Object.NaturalNumbers
open import Categories.Category.Cartesian

-- open import Categories.Category.Construction.F-Algebras
-- open import Categories.Object.NaturalNumbers.Parametrized.Properties.F-Algebras

open import Categories.Object.Exponential using (Exponential)

import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR

module Monad.Instance.Delay.Retract {o ℓ e} {C : Category o ℓ e}
    (distributive : Distributive C)
    (DM : DelayM (Distributive.cocartesian distributive))
    (nno : NNO C (Cartesian.terminal (Distributive.cartesian distributive)))
    (ℕ^ : ∀ X → Exponential C (NNO.N nno) X) where
    
    open Category C
    -- open Distributive distributive
    open import Category.Distributive.Helper distributive
    -- open Bundles
    open DelayM DM
    open HomReasoning
    open Equiv
    -- open D-Monad
    -- open D-Kleisli
    -- open Later∘Extend
    -- open Coit

    -- open M C
    -- open MR C

    open NNO 
    open Terminal terminal renaming (⊤ to ı)
    open import Object.NaturalNumbers.Primitive cartesian coproducts nno

    open Exponential using (λg; B^A)

    module _ {X : Obj} where

      D-to-stream : D₀ X ⇒ B^A (ℕ^(X + ı))
      D-to-stream = λg (ℕ^(X + ı)) product {!NNO-universal-primitive!}
      --(universal (( id +₁ !) ∘ out) {!!}) --  ([ {!( id +₁ !) ∘ out!} , i₂ ]))