{-# OPTIONS --allow-unsolved-metas #-}
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
    open Terminal terminal
    -- ι
    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 
        ι                   ≈⟨ unique (sym ι-zero) (sym ι-succ) ⟩ 
        universal now later ≈˘⟨ 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)              ≈⟨ unique (sym IB₁) (sym IS₁) ⟩ 
      universal (now ∘ f) later ≈˘⟨ 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₂ refl 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)))