{-# 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.Parametrized
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))
    (pnno : ParametrizedNNO C (Distributive.cartesian distributive))
    (_^ℕ : ∀ X → Exponential C (ParametrizedNNO.N pnno) X) where
    
    open Category C
    -- open Distributive distributive
    open import Categories.Object.Product.Core C using (repack)
    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 ParametrizedNNO 
    open Terminal terminal renaming (⊤ to ı)
    open import Object.NaturalNumbers.Parametrized.Primitive cartesian coproducts pnno

    open Exponential using (λg; eval; B^A)

    module _ {X : Obj} where

      D-to-stream : D₀ X ⇒ B^A ((X + ı)^ℕ)
      D-to-stream = λg ((X + ı)^ℕ) product (( id +₁ !) ∘ out ∘ universal pnno id ( [ now , id ] ∘ out ))

      D-retract : Retract (B^A ((X + ı)^ℕ)) (D₀ X)
      D-retract .M.Retract.section = Coit.coit ((π₁ +₁ λg ((X + ı)^ℕ) product
        (eval ((X + ı) ^ℕ) ∘ repack product (Exponential.product ((X + ı)^ℕ)) ∘ (id ⁂ s pnno)) ∘ π₂) ∘
        distributeʳ⁻¹ ∘ ⟨ eval ((X + ı)^ℕ) ∘ repack product (Exponential.product ((X + ı)^ℕ)) ∘ ⟨ id , z pnno ∘ ! ⟩ , id ⟩) 

      D-retract .M.Retract.retract = D-to-stream
      D-retract .M.Retract.is-retract = {!!}