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 ⟩