open import Categories.Category
open import Monad.Instance.Delay
open import Categories.Monad.Relative using () renaming (Monad to RMonad)
open import Categories.Category.Distributive
open import Categories.Object.Terminal
open import Categories.Object.NaturalNumbers.Parametrized
open import Categories.Category.Construction.F-Algebras
open import Categories.Object.NaturalNumbers.Parametrized.Properties.F-Algebras

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

module Monad.Instance.Delay.Iota {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (DM : DelayM (Distributive.cocartesian distributive)) (PNNO : ParametrizedNNO C (Distributive.cartesian distributive)) 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 ParametrizedNNO PNNO renaming (unique to pnno-unique)

    module _ {X : Obj} where
      nno-iso : X × N ≅ X + X × N
      nno-iso = Lambek.lambek (record { ⊥ = PNNO-Algebra C cartesian coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ C cartesian coproducts PNNO X })

      ι : X × N ⇒ D.F.₀ X
      ι = coit (_≅_.from nno-iso)

      ι-commutes : out ∘ ι ≈ (id +₁ ι) ∘ _≅_.from nno-iso
      ι-commutes = coit-commutes (_≅_.from nno-iso)

      ι-zero : ι ∘ ⟨ id , z ∘ ! ⟩ ≈ now
      ι-zero = begin 
        ι ∘ ⟨ id , z ∘ ! ⟩                                              ≈⟨ cancelˡ out⁻¹∘out ⟨  
        out⁻¹ ∘ out ∘ ι ∘ ⟨ id , z ∘ ! ⟩                                ≈⟨ refl⟩∘⟨ (extendʳ ι-commutes) ⟩ 
        out⁻¹ ∘ (id +₁ ι) ∘ _≅_.from nno-iso ∘ ⟨ id , z ∘ ! ⟩          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ commute₁ ⟨  
        out⁻¹ ∘ (id +₁ ι) ∘ (id +₁ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ]) ∘ i₁    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (inject₁ ○ identityʳ) ⟩ 
        out⁻¹ ∘ (id +₁ ι) ∘ i₁                                          ≈⟨ refl⟩∘⟨ (inject₁ ○ identityʳ) ⟩ 
        now                                                             ∎

      ι-succ : ι ∘ (id ⁂ s) ≈ later ∘ ι
      ι-succ = begin 
        ι ∘ (id ⁂ s)                                                                          ≈⟨ cancelˡ out⁻¹∘out ⟨ 
        out⁻¹ ∘ out ∘ ι ∘ (id ⁂ s)                                                            ≈⟨ refl⟩∘⟨ (extendʳ ι-commutes) ⟩ 
        out⁻¹ ∘ (id +₁ ι) ∘ _≅_.from nno-iso ∘ (id ⁂ s)                                      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ commute₂ ⟨ 
        out⁻¹ ∘ (id +₁ ι) ∘ ((id +₁ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ]) ∘ i₂) ∘ _≅_.from nno-iso    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ inject₂ ⟩∘⟨refl ⟩ 
        out⁻¹ ∘ (id +₁ ι) ∘ (i₂ ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ]) ∘ _≅_.from nno-iso            ≈⟨ refl⟩∘⟨ (pullˡ (pullˡ inject₂)) ⟩ 
        out⁻¹ ∘ ((i₂ ∘ ι) ∘ _≅_.to nno-iso) ∘ _≅_.from nno-iso                              ≈⟨ refl⟩∘⟨ cancelʳ (_≅_.isoˡ nno-iso) ⟩ 
        out⁻¹ ∘ (i₂ ∘ ι)                                                                      ≈⟨ sym-assoc ⟩ 
        later ∘ ι                                                                             ∎

      ι-unique : ∀ (f : X × N ⇒ D.F.₀ X) 
        → f ∘ ⟨ id , z ∘ ! ⟩             ≈ now 
        → f ∘ (id ⁂ s)                   ≈ later ∘ f
        → ι                              ≈ f
      ι-unique f f-zero f-succ = begin 
        ι                                ≈⟨ pnno-unique (sym ι-zero) (sym ι-succ) ⟩
        universal now later              ≈⟨ pnno-unique (sym f-zero) (sym f-succ) ⟨
        f                                ∎

    ι-natural : ∀ {X Y} (f : X ⇒ Y) → ι ∘ (f ⁂ id) ≈ D.F.₁ f ∘ ι
    ι-natural {X} {Y} f = begin 
      ι ∘ (f ⁂ id)                 ≈⟨ pnno-unique (sym IB₁) (sym IS₁) ⟩
      universal (now ∘ f) later    ≈⟨ pnno-unique (sym IB₂) (sym IS₂) ⟨
      D.F.₁ f ∘ ι                  ∎
        where
          IB₁ : (ι ∘ (f ⁂ id)) ∘ ⟨ id , z ∘ ! ⟩ ≈ now ∘ f
          IB₁ = begin 
            (ι ∘ (f ⁂ id)) ∘ ⟨ id , z ∘ ! ⟩     ≈⟨ pullʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ id-comm (identityˡ ○ ∘-resp-≈ʳ (!-unique (! ∘ f)))) ⟩
            ι ∘ ⟨ id ∘ f , z ∘ ! ∘ f ⟩          ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congˡ assoc) ⟨ 
            ι ∘ ⟨ id , z ∘ ! ⟩ ∘ f              ≈⟨ pullˡ ι-zero ⟩
            now ∘ f                             ∎
          
          IS₁ : (ι ∘ (f ⁂ id)) ∘ (id ⁂ s) ≈ later ∘ ι ∘ (f ⁂ id)
          IS₁ = begin 
            (ι ∘ (f ⁂ id)) ∘ (id ⁂ s)             ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm id-comm-sym ○ sym ⁂∘⁂) ⟩ 
            ι ∘ (id ⁂ s) ∘ (f ⁂ id)               ≈⟨ extendʳ ι-succ ⟩ 
            later ∘ ι ∘ (f ⁂ id)                  ∎

          IB₂ : (D.F.₁ f ∘ ι) ∘ ⟨ id , z ∘ ! ⟩ ≈ now ∘ f
          IB₂ = pullʳ ι-zero ○ sym (D.η.commute f)

          IS₂ : (D.F.₁ f ∘ ι) ∘ (id ⁂ s) ≈ later ∘ D.F.₁ f ∘ ι
          IS₂ = pullʳ ι-succ ○ extendʳ (sym (later-extend-comm (now ∘ f)))

    ι̂ : N ⇒ D.F.₀ ⊤
    ι̂ = ι ∘ ⟨ ! , id ⟩