{-# OPTIONS --allow-unsolved-metas #-}
module Kleisli where

open import Base
open import Monoidal
open import Concurrent

Kleisli-P : (ℂ : MonoidalCategory) (T : ConcurrentMonad ℂ)
                        → ParamCategory (MonoidalCategory.obj ℂ)
Kleisli-P ℂ T =
  let open MonoidalCategory ℂ
      open ConcurrentMonad T renaming (F₀ to T₀ ; F₁ to T₁)
      module T = ConcurrentMonad T
  in record
    { hom = λ X Y → hom X (T₀ Y)
    ; id = λ X → η-at X
    ; _▷_ = λ {X} {Y} {Z} xfy yfz → xfy ▷ T₁ yfz ▷ μ-at Z
    ; _≤_ = λ xfy xfy' → xfy ≤ xfy'
    ; ▷lunit = λ {X} {Y} {f} →
      begin
        η-at X ▷ T₁ f ▷ μ-at Y
      ≡⟨ sym ▷assoc ⟩
        (η-at X ▷ T₁ f) ▷ μ-at Y
      ≡⟨ cong (λ x → x ▷ μ-at Y) (sym η-naturality) ⟩
       (f ▷ η-at (T₀ Y)) ▷ μ-at Y
      ≡⟨ ▷assoc ⟩
        (f ▷ η-at (T₀ Y) ▷ μ-at Y)
      ≡⟨ cong (λ X → f ▷ X) diagram1 ⟩
        (f ▷ id (T₀ Y))
      ≡⟨ sym ▷runit ⟩
        f
      ∎
    ; ▷runit = λ {X} {Y} {f} →
      begin
        f
      ≡⟨ ▷runit ⟩
        f ▷ id (T₀ Y)
      ≡⟨ cong (λ x → f ▷ x) (sym diagram2) ⟩
        f ▷ T₁ (η-at Y) ▷ μ-at Y
      ∎
    ; ▷assoc = λ {X} {Y} {Z} {W} {f} {g} {h} →
      begin
        (f ▷ T₁ g ▷ μ-at Z) ▷ T₁ h ▷ μ-at W
      ≡⟨ ▷assoc ⟩
        f ▷ (T₁ g ▷ μ-at Z) ▷ T₁ h ▷ μ-at W
      ≡⟨ cong (λ x → f ▷ x) ▷assoc ⟩
        f ▷ T₁ g ▷ μ-at Z ▷ T₁ h ▷ μ-at W
      ≡⟨ cong (λ x → f ▷ T₁ g ▷ x) (sym ▷assoc) ⟩
        f ▷ T₁ g ▷ (μ-at Z ▷ T₁ h) ▷ μ-at W
      ≡⟨ cong (λ x → f ▷ T₁ g ▷ x ▷ μ-at W) (sym μ-naturality) ⟩
        f ▷ T₁ g ▷ (T₁ (T₁ h) ▷ μ-at (T₀ W)) ▷ μ-at W
      ≡⟨ cong (λ x → f ▷ T₁ g ▷ x) ▷assoc ⟩
        f ▷ T₁ g ▷ T₁ (T₁ h) ▷ μ-at (T₀ W) ▷ μ-at W
      ≡⟨ cong (λ x → f ▷ T₁ g ▷ T₁ (T₁ h) ▷ x) (sym diagram3) ⟩
        f ▷ T₁ g ▷ T₁ (T₁ h) ▷ T₁ (μ-at W) ▷ μ-at W
      ≡⟨ cong (λ x → f ▷ x) (sym ▷assoc) ⟩
        f ▷ (T₁ g ▷ T₁ (T₁ h)) ▷ T₁ (μ-at W) ▷ μ-at W
      ≡⟨ cong (λ x → f ▷ x) (sym ▷assoc) ⟩
        f ▷ ((T₁ g ▷ T₁ (T₁ h)) ▷ T₁ (μ-at W)) ▷ μ-at W
      ≡⟨ cong (λ x → f ▷ x ▷ μ-at W) ▷assoc ⟩
        f ▷ (T₁ g ▷ T₁ (T₁ h) ▷ T₁ (μ-at W)) ▷ μ-at W
      ≡⟨ cong (λ x → f ▷ (T₁ g ▷ x) ▷ μ-at W) (sym T.strictComposition) ⟩
        f ▷ (T₁ g ▷ T₁ (T₁ h ▷ μ-at W)) ▷ μ-at W
      ≡⟨  cong (λ x → f ▷ x ▷ μ-at W) (sym T.strictComposition) ⟩
        f ▷ T₁ (g ▷ T₁ h ▷ μ-at W) ▷ μ-at W
      ∎
    ; ≤refl = ≤refl
    ; ≤trans = ≤trans
    ; ≤antisym = ≤antisym
    ; ▷monot≤ = λ ff' gg' → ▷monot≤ ff' (▷monot≤ (T.preserveOrder gg') ≤refl)
    }
        

Kleisli-MonoidalLikeProduct : (ℂ : MonoidalCategory) (T : ConcurrentMonad ℂ)
  → ParamLaxFunctor (ParamProduct (Kleisli-P ℂ T)
                                  (Kleisli-P ℂ T))
                    (Kleisli-P ℂ T)
                    (MonoidalCategory.MonoidalProduct₀ ℂ)
Kleisli-MonoidalLikeProduct ℂ T =
  let open MonoidalCategory ℂ
      open ConcurrentMonad T renaming (F₀ to T₀ ; F₁ to T₁)
      module T = ConcurrentMonad T
  in record
    { prefunctor = record
      { F₁ = λ {_} {(B , D)} (f , g) → f ⊗₁ g ▷ ψ-at B D
      ; preserveOrder = λ {X} {Y} {f} {g} (fg , fg') →
          ▷monot≤ (MonoidalProduct.preserveOrder (fg , fg')) ≤refl
      }
    ; isParamLaxFunctor = record
      { laxIdentity = λ {X} → inequation3
      ; laxComposition = λ {(A , D)} {(B , E)} {(C , F)} {(f , g)} {(f' , g')} →
        let open ≤-Reasoning {ℂ} {_} {_} in
        ≤begin
          (f ⊗₁ g ▷ ψ-at B E) ▷ T₁ (f' ⊗₁ g' ▷ ψ-at C F) ▷ μ-at (C ⊗ F)
        ≦⟨ ▷assoc ⟩
          f ⊗₁ g ▷ ψ-at B E ▷ T₁ (f' ⊗₁ g' ▷ ψ-at C F) ▷ μ-at (C ⊗ F)
        ≦⟨ cong (λ x → f ⊗₁ g ▷ ψ-at B E ▷ x ▷ μ-at (C ⊗ F)) T.strictComposition ⟩
          f ⊗₁ g ▷ ψ-at B E ▷ (T₁ (f' ⊗₁ g') ▷ T₁ (ψ-at C F)) ▷ μ-at (C ⊗ F)
        ≦⟨ cong (λ x → f ⊗₁ g ▷ ψ-at B E ▷ x) ▷assoc ⟩
          f ⊗₁ g ▷ ψ-at B E ▷ T₁ (f' ⊗₁ g') ▷ T₁ (ψ-at C F) ▷ μ-at (C ⊗ F)
        ≦⟨ cong (λ x → f ⊗₁ g ▷ x) (sym ▷assoc) ⟩
          f ⊗₁ g ▷ (ψ-at B E ▷ T₁ (f' ⊗₁ g')) ▷ T₁ (ψ-at C F) ▷ μ-at (C ⊗ F)
        ≦⟨ cong (λ x → f ⊗₁ g ▷ x ▷ T₁ (ψ-at C F) ▷ μ-at (C ⊗ F)) (sym (ψ-naturality)) ⟩
          f ⊗₁ g ▷ (T₁ f' ⊗₁ T₁ g' ▷ ψ-at (T₀ C) (T₀ F)) ▷ T₁ (ψ-at C F) ▷ μ-at (C ⊗ F)
        ≦⟨ cong (λ x → f ⊗₁ g ▷ x) ▷assoc ⟩
          f ⊗₁ g ▷ T₁ f' ⊗₁ T₁ g' ▷ ψ-at (T₀ C) (T₀ F) ▷ T₁ (ψ-at C F) ▷ μ-at (C ⊗ F)
        ≦⟨ sym ▷assoc ⟩
          ((f ⊗₁ g ▷ T₁ f' ⊗₁ T₁ g') ▷ ψ-at (T₀ C) (T₀ F) ▷ T₁ (ψ-at C F) ▷ μ-at (C ⊗ F))
        ≤⟨ ▷monot≤ (≤refl {_} {_} {f ⊗₁ g ▷ T₁ f' ⊗₁ T₁ g'}) inequation4 ⟩
         (f ⊗₁ g ▷ T₁ f' ⊗₁ T₁ g') ▷ μ-at C ⊗₁ μ-at F ▷ ψ-at C F
        ≦⟨ cong (λ x → x ▷ _ ▷ _) (sym MonoidalProduct.strictComposition) ⟩
         (f ▷ T₁ f') ⊗₁ (g ▷ T₁ g') ▷ μ-at C ⊗₁ μ-at F ▷ ψ-at C F
        ≦⟨ sym ▷assoc ⟩
          ((f ▷ T₁ f') ⊗₁ (g ▷ T₁ g') ▷ μ-at C ⊗₁ μ-at F) ▷ ψ-at C F
        ≦⟨ cong (λ x → x ▷ ψ-at C F) (sym MonoidalProduct.strictComposition) ⟩
          ((f ▷ T₁ f') ▷ μ-at C) ⊗₁ ((g ▷ T₁ g') ▷ μ-at F) ▷ ψ-at C F
        ≦⟨ cong (λ x → x ⊗₁ ((_ ▷ T₁ g') ▷ μ-at F) ▷ _) ▷assoc ⟩
          ((f ▷ T₁ f' ▷ μ-at C) ⊗₁ ((g ▷ T₁ g') ▷ μ-at F) ▷ ψ-at C F)
        ≦⟨ cong (λ x → (_ ▷ T₁ f' ▷ μ-at C) ⊗₁ x ▷ _) ▷assoc ⟩
          (f ▷ T₁ f' ▷ μ-at C) ⊗₁ (g ▷ T₁ g' ▷ μ-at F) ▷ ψ-at C F
        ≤∎
      }
    }

Kleisli-LikeI : (ℂ : MonoidalCategory) (T : ConcurrentMonad ℂ)
  → ParamLaxFunctor 𝟙 (Kleisli-P ℂ T) (MonoidalCategory.Identity₀ ℂ)
Kleisli-LikeI ℂ T =
  let open MonoidalCategory ℂ
      open ConcurrentMonad T renaming (F₀ to T₀ ; F₁ to T₁)
  in record
    { prefunctor = record
      { F₁ = λ { tt → ψ⁰ }
      ; preserveOrder = λ x → ≤refl
      }
    ; isParamLaxFunctor = record
      { laxIdentity = inequation1
      ; laxComposition = inequation2
      }
    }

Kleisli-isPMLC : (ℂ : MonoidalCategory) (T : ConcurrentMonad ℂ)
                            → IsParamMonoidalLikeCategory
                                (Kleisli-P ℂ T)
                                (Kleisli-MonoidalLikeProduct ℂ T)
                                (Kleisli-LikeI ℂ T)
Kleisli-isPMLC ℂ T =
  let open MonoidalCategory ℂ
      open ConcurrentMonad T renaming (F₀ to T₀ ; F₁ to T₁)
      module T = ConcurrentMonad T
      𝕂-▷lunit = ParamCategory.▷lunit (Kleisli-P ℂ T)
  in record { }

Kleisli-𝕂 : (ℂ : MonoidalCategory) (T : ConcurrentMonad ℂ) → ParamMonoidalLikeCategory
                             (MonoidalCategory.obj ℂ)
                             (MonoidalCategory.MonoidalProduct₀ ℂ)
                             (MonoidalCategory.Identity₀ ℂ)
Kleisli-𝕂 ℂ T =
  let open MonoidalCategory ℂ
      open ConcurrentMonad T
  in record
    { P = Kleisli-P ℂ T
    ; MonoidalLikeProduct = Kleisli-MonoidalLikeProduct ℂ T
    ; funcLikeI = Kleisli-LikeI ℂ T
    ; isParamMonoidalLikeCategory = Kleisli-isPMLC ℂ T
    }
    

Kleisli-J : (ℂ : MonoidalCategory) (T : ConcurrentMonad ℂ)
                       → JFunctor (MonoidalCategory.P-monoidal ℂ) (Kleisli-𝕂 ℂ T)
Kleisli-J ℂ monT =
  let open MonoidalCategory ℂ
      open ConcurrentMonad monT renaming (F₁ to T₁ ; F₀ to T; strictComposition to TstrictComposition)
      𝕂-▷lunit = ParamCategory.▷lunit (Kleisli-P ℂ monT)
      t : ∀ {A B f} → λ-at A ▷ f ≡ (ψ⁰ ⊗₁ f ▷ ψ-at I B) ▷ T₁ (λ-at B ▷ η-at B) ▷ μ-at B
      t = λ {A B f} →
          begin 
            λ-at A ▷ f
          ≡⟨ sym (λ-naturality f) ⟩
            I₁ ⊗₁ f ▷ λ-at (T B)
          ≡⟨ cong (λ x → I₁ ⊗₁ f ▷ x) diagram4 ⟩
            I₁ ⊗₁ f ▷ ψ⁰ ⊗₁ id (T B) ▷ ψ-at I B ▷ T₁ (λ-at B)
          ≡⟨ sym ▷assoc ⟩
            (I₁ ⊗₁ f ▷ ψ⁰ ⊗₁ id (T B)) ▷ ψ-at I B ▷ T₁ (λ-at B)
          ≡⟨ cong (λ x → x ▷ ψ-at I B ▷ T₁ (λ-at B)) (sym MonoidalProduct.strictComposition) ⟩
            (I₁ ▷ ψ⁰) ⊗₁ (f ▷ id (T B)) ▷ ψ-at I B ▷ T₁ (λ-at B)
          ≡⟨ cong (λ x → (I₁ ▷ ψ⁰) ⊗₁ x ▷ ψ-at I B ▷ T₁ (λ-at B)) (sym ▷runit) ⟩
            (I₁ ▷ ψ⁰) ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)
          ≡⟨ cong (λ x → (x ▷ ψ⁰) ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)) funcI.strictIdentity ⟩
            (id I ▷ ψ⁰) ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)
          ≡⟨ cong (λ x → x ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)) ▷lunit ⟩
            ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)
          ≡⟨ ▷runit ⟩
            (ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)) ▷ id (T B)
          ≡⟨ cong (λ x → (ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)) ▷ x) (sym diagram2) ⟩
            (ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)) ▷ T₁ (η-at B) ▷ μ-at B
          ≡⟨ ▷assoc ⟩
            ψ⁰ ⊗₁ f ▷ (ψ-at I B ▷ T₁ (λ-at B)) ▷ T₁ (η-at B) ▷ μ-at B
          ≡⟨ cong (λ x → ψ⁰ ⊗₁ f ▷ x) ▷assoc ⟩
            ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B) ▷ T₁ (η-at B) ▷ μ-at B
          ≡⟨ cong (λ x → ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ x) (sym ▷assoc) ⟩
            ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ (T₁ (λ-at B) ▷ T₁ (η-at B)) ▷ μ-at B
          ≡⟨ cong (λ x → ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ x ▷ μ-at B) (sym TstrictComposition) ⟩
            ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B ▷ η-at B) ▷ μ-at B
          ≡⟨ sym ▷assoc ⟩
            (ψ⁰ ⊗₁ f ▷ ψ-at I B) ▷ T₁ (λ-at B ▷ η-at B) ▷ μ-at B
          ∎
      ρ-naturality = λ {A B f} →
          begin
            (ρ-at A ▷ η-at (A ⊗ I)) ▷ T₁ (f ⊗₁ ψ⁰ ▷ ψ-at B I) ▷ μ-at (B ⊗ I)
          ≡⟨ ▷assoc ⟩
            ρ-at A ▷ η-at (A ⊗ I) ▷ T₁ (f ⊗₁ ψ⁰ ▷ ψ-at B I) ▷ μ-at (B ⊗ I)
          ≡⟨ cong (λ x → ρ-at A ▷ x) 𝕂-▷lunit ⟩
            ρ-at A ▷ f ⊗₁ ψ⁰ ▷ ψ-at B I
          ≡⟨ cong (λ x → ρ-at A ▷ x ⊗₁ ψ⁰ ▷ ψ-at B I) ▷runit ⟩
            ρ-at A ▷ (f ▷ id (T B)) ⊗₁ ψ⁰ ▷ ψ-at B I
          ≡⟨ cong (λ x → ρ-at A ▷ (f ▷ id (T B)) ⊗₁ x ▷ ψ-at B I) (sym ▷lunit) ⟩
            ρ-at A ▷ (f ▷ id (T B)) ⊗₁ (id I ▷ ψ⁰) ▷ ψ-at B I
          ≡⟨ cong (λ x → ρ-at A ▷ x ▷ ψ-at B I) MonoidalProduct.strictComposition ⟩
            ρ-at A ▷ (f ⊗₁ id I ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I
          ≡⟨ sym ▷assoc ⟩
            (ρ-at A ▷ f ⊗₁ id I ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I
          ≡⟨ cong (λ x → x ▷ ψ-at B I) (sym ▷assoc) ⟩
            ((ρ-at A ▷ f ⊗₁ id I) ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I
          ≡⟨ cong (λ x → ((ρ-at A ▷ f ⊗₁ x) ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I) (sym funcI.strictIdentity) ⟩
            (((ρ-at A ▷ f ⊗₁ I₁) ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I)
          ≡⟨ cong (λ x → (x ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I) (ℂ.ρ-naturality f) ⟩
            ((f ▷ ρ-at (T B)) ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I
          ≡⟨ ▷assoc ⟩
            (f ▷ ρ-at (T B)) ▷ id (T B) ⊗₁ ψ⁰ ▷ ψ-at B I
          ≡⟨ ▷assoc ⟩
            f ▷ ρ-at (T B) ▷ id (T B) ⊗₁ ψ⁰ ▷ ψ-at B I
          ≡⟨ cong (λ x → f ▷ x) diagram5 ⟩
            f ▷ T₁ (ρ-at B)
          ≡⟨ ▷runit ⟩
            (f ▷ T₁ (ρ-at B)) ▷ id (T (B ⊗ I))
          ≡⟨ cong (λ x → _ ▷ x) (sym diagram2) ⟩
            (f ▷ T₁ (ρ-at B)) ▷ T₁ (η-at (B ⊗ I)) ▷ μ-at (B ⊗ I)
          ≡⟨ ▷assoc ⟩
            f ▷ T₁ (ρ-at B) ▷ T₁ (η-at (B ⊗ I)) ▷ μ-at (B ⊗ I)
          ≡⟨ cong (λ x → f ▷ x) (sym ▷assoc) ⟩
            f ▷ (T₁ (ρ-at B) ▷ T₁ (η-at (B ⊗ I))) ▷ μ-at (B ⊗ I)
          ≡⟨ cong (λ x → f ▷ x ▷ μ-at _) (sym TstrictComposition) ⟩
            f ▷ T₁ (ρ-at B ▷ η-at (B ⊗ I)) ▷ μ-at (B ⊗ I)
          ∎
  in record
    { F = record
      { prefunctor = record
        { F₁ = λ {X} {Y} z → z ▷ η-at Y
        ; preserveOrder = λ {X} {Y} {f} {g} z → ▷monot≤ z ≤refl
        }
      ; isParamFunctor = record
        { strictIdentity = λ {X} → ▷lunit
        ; strictComposition = λ {X} {Y} {Z} {f} {g} →
          begin
            (f ▷ g) ▷ η-at Z
          ≡⟨ ▷assoc ⟩
            f ▷ (g ▷ η-at Z)
          ≡⟨ cong (λ x → _ ▷ x) (sym 𝕂-▷lunit) ⟩
            f ▷ η-at Y ▷ T₁ (g ▷ η-at Z) ▷ μ-at Z
          ≡⟨ sym ▷assoc ⟩
            (f ▷ η-at Y) ▷ T₁ (g ▷ η-at Z) ▷ μ-at Z
          ∎
        }
      }
    ; isJOplaxMonoidalFunctor = record
      { ω-at = λ A B → η-at (A ⊗ B)
      ; ω-naturality = λ {A} {B} {C} {D} {f} {g} →
        let open ≤-Reasoning {ℂ} in
        ≤begin
          (f ⊗₁ g ▷ η-at (B ⊗ D)) ▷ T₁ (η-at (B ⊗ D)) ▷ μ-at (B ⊗ D)
        ≦⟨ ▷assoc ⟩
          f ⊗₁ g ▷ η-at (B ⊗ D) ▷ T₁ (η-at (B ⊗ D)) ▷ μ-at (B ⊗ D)
        ≦⟨ cong (λ x → f ⊗₁ g ▷ x) 𝕂-▷lunit ⟩
          f ⊗₁ g ▷ η-at (B ⊗ D)
        ≤⟨ ▷monot≤ ≤refl inequation3 ⟩
          f ⊗₁ g ▷ η-at B ⊗₁ η-at D ▷ ψ-at B D
        ≦⟨ sym ▷assoc ⟩
          (f ⊗₁ g ▷ η-at B ⊗₁ η-at D) ▷ ψ-at B D
        ≦⟨ cong (λ x → x ▷ ψ-at B D) (sym MonoidalProduct.strictComposition) ⟩
          (f ▷ η-at B) ⊗₁ (g ▷ η-at D) ▷ ψ-at B D
        ≦⟨ sym 𝕂-▷lunit ⟩
          η-at (A ⊗ C) ▷ T₁ ((f ▷ η-at B) ⊗₁ (g ▷ η-at D) ▷ ψ-at B D) ▷ μ-at (B ⊗ D)
        ≤∎
      ; ω⁰ = ψ⁰
      ; oplaxAssoc = λ {X} {Y} {Z} →
        begin
          η-at ((X ⊗ Y) ⊗ Z) ▷ T₁ ((η-at (X ⊗ Y) ⊗₁ η-at Z ▷ ψ-at (X ⊗ Y) Z) ▷ T₁ (α-at X Y Z ▷ η-at (X ⊗ (Y ⊗ Z))) ▷ μ-at (X ⊗ (Y ⊗ Z))) ▷ μ-at (X ⊗ (Y ⊗ Z))
        ≡⟨ 𝕂-▷lunit ⟩
          (η-at (X ⊗ Y) ⊗₁ η-at Z ▷ ψ-at (X ⊗ Y) Z) ▷ T₁ (α-at X Y Z ▷ η-at (X ⊗ Y ⊗ Z)) ▷ μ-at (X ⊗ Y ⊗ Z)
        ≡⟨ {!!} ⟩
          α-at X Y Z ▷ η-at (X ⊗ Y ⊗ Z) ▷ T₁ (η-at X ⊗₁ η-at (Y ⊗ Z) ▷ ψ-at X (Y ⊗ Z)) ▷ μ-at (X ⊗ Y ⊗ Z)
        ≡⟨ cong (λ x → α-at X Y Z ▷ x) (sym 𝕂-▷lunit) ⟩
          α-at X Y Z ▷ η-at (X ⊗ Y ⊗ Z) ▷ T₁ (η-at (X ⊗ Y ⊗ Z) ▷ T₁ (η-at X ⊗₁ η-at (Y ⊗ Z) ▷ ψ-at X (Y ⊗ Z)) ▷ μ-at (X ⊗ Y ⊗ Z)) ▷ μ-at (X ⊗ Y ⊗ Z)
        ≡⟨ sym ▷assoc ⟩
          (α-at X Y Z ▷ η-at (X ⊗ (Y ⊗ Z))) ▷ T₁ (η-at (X ⊗ Y ⊗ Z) ▷ T₁ (η-at X ⊗₁ η-at (Y ⊗ Z) ▷ ψ-at X (Y ⊗ Z)) ▷ μ-at (X ⊗ (Y ⊗ Z))) ▷ μ-at (X ⊗ (Y ⊗ Z))
        ∎ 
      -- found an inequality using lunit twice and inequation 1 and diagram4
      ; oplaxLunital = λ {X} →
        begin
          λ-at X ▷ η-at X
        ≡⟨ sym 𝕂-▷lunit ⟩
          η-at (I ⊗ X) ▷ T₁ (λ-at X ▷ η-at X) ▷ μ-at X
        ≡⟨ cong (λ x → η-at (I ⊗ X) ▷ T₁ x ▷ μ-at X) t ⟩
          η-at (I ⊗ X) ▷ T₁ ((ψ⁰ ⊗₁ η-at X ▷ ψ-at I X) ▷ T₁ (λ-at X ▷ η-at X) ▷ μ-at X) ▷ μ-at X
        ∎
      -- need inequation3, inequation1 and lunit for an inequality
      ; oplaxRunital = λ {X} →
        begin
          ρ-at X ▷ η-at (X ⊗ I)
        ≡⟨ sym 𝕂-▷lunit ⟩
          η-at _ ▷ T₁ (ρ-at X ▷ η-at (X ⊗ I)) ▷ μ-at _
        ≡⟨ sym ρ-naturality ⟩
          (ρ-at X ▷ η-at (X ⊗ I)) ▷ T₁ (η-at X ⊗₁ ψ⁰ ▷ ψ-at X I) ▷ μ-at (X ⊗ ℂ.I)
        ≡⟨ cong (λ x → _ ▷ T₁ x ▷ _) (sym 𝕂-▷lunit) ⟩
          (ρ-at X ▷ η-at (X ⊗ I)) ▷ T₁ (η-at (X ⊗ I) ▷ T₁ ((η-at X ⊗₁ ψ⁰) ▷ ψ-at X I)
            ▷ μ-at (X ⊗ I)) ▷ μ-at (X ⊗ I)
        ∎
      ; preserveI₁ = let open ≤-Reasoning {ℂ} in
        ≤begin
           I₁ ▷ η-at I
        ≦⟨ cong (λ x → x ▷ η-at I) funcI.strictIdentity ⟩
           id I ▷ η-at I
        ≦⟨ ▷lunit ⟩
           η-at I
        ≤⟨ inequation1 ⟩
          ψ⁰
        ≤∎
      ; preserve⊗₁ = λ {X} {Y} {U} {V} f g → let open ≤-Reasoning {ℂ} in
        ≤begin
          f ⊗₁ g ▷ η-at (Y ⊗ V)
        ≤⟨ ▷monot≤ ≤refl inequation3 ⟩
          f ⊗₁ g ▷ η-at Y ⊗₁ η-at V ▷ ψ-at Y V
        ≦⟨ sym ▷assoc ⟩
          (f ⊗₁ g ▷ η-at Y ⊗₁ η-at V) ▷ ψ-at Y V
        ≦⟨ cong (λ x → x ▷ ψ-at Y V) (sym MonoidalProduct.strictComposition) ⟩
          (f ▷ η-at Y) ⊗₁ (g ▷ η-at V) ▷ ψ-at Y V
        ≤∎
      }
    }

Kleisli-MonoidalLikeCategory : (ℂ : MonoidalCategory) (T : ConcurrentMonad ℂ) → MonoidalLikeCategory
Kleisli-MonoidalLikeCategory ℂ T =
  record
    { c = MonoidalCategory.obj ℂ
    ; t⊗₀ = MonoidalCategory.MonoidalProduct₀ ℂ
    ; tI₀ = MonoidalCategory.Identity₀ ℂ
    ; P-monoidallike = Kleisli-𝕂 ℂ T
    }

Kleisli-isConcurrentCategory : (ℂ : MonoidalCategory) (T : ConcurrentMonad ℂ)
  → IsConcurrentCategory (MonoidalCategory.P-monoidal ℂ)
                         (Kleisli-𝕂 ℂ T)
                         (Kleisli-J ℂ T)
Kleisli-isConcurrentCategory ℂ monT =
  let 
      open ConcurrentMonad monT renaming (F₀ to T; F₁ to T₁; strictComposition to TstrictComposition; diagram2 to diagram2)
      open MonoidalCategory ℂ
      𝕂-▷lunit = ParamCategory.▷lunit (Kleisli-P ℂ monT)
      t : ∀ {A B f} → λ-at A ▷ f ≡ (ψ⁰ ⊗₁ f ▷ ψ-at I B) ▷ T₁ (λ-at B ▷ η-at B) ▷ μ-at B
      t = λ {A B f} →
          begin 
            λ-at A ▷ f
          ≡⟨ sym (λ-naturality f) ⟩
            I₁ ⊗₁ f ▷ λ-at (T B)
          ≡⟨ cong (λ x → I₁ ⊗₁ f ▷ x) diagram4 ⟩
            I₁ ⊗₁ f ▷ ψ⁰ ⊗₁ id (T B) ▷ ψ-at I B ▷ T₁ (λ-at B)
          ≡⟨ sym ▷assoc ⟩
            (I₁ ⊗₁ f ▷ ψ⁰ ⊗₁ id (T B)) ▷ ψ-at I B ▷ T₁ (λ-at B)
          ≡⟨ cong (λ x → x ▷ ψ-at I B ▷ T₁ (λ-at B)) (sym MonoidalProduct.strictComposition) ⟩
            (I₁ ▷ ψ⁰) ⊗₁ (f ▷ id (T B)) ▷ ψ-at I B ▷ T₁ (λ-at B)
          ≡⟨ cong (λ x → (I₁ ▷ ψ⁰) ⊗₁ x ▷ ψ-at I B ▷ T₁ (λ-at B)) (sym ▷runit) ⟩
            (I₁ ▷ ψ⁰) ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)
          ≡⟨ cong (λ x → (x ▷ ψ⁰) ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)) funcI.strictIdentity ⟩
            (id I ▷ ψ⁰) ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)
          ≡⟨ cong (λ x → x ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)) ▷lunit ⟩
            ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)
          ≡⟨ ▷runit ⟩
            (ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)) ▷ id (T B)
          ≡⟨ cong (λ x → (ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)) ▷ x) (sym diagram2) ⟩
            (ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B)) ▷ T₁ (η-at B) ▷ μ-at B
          ≡⟨ ▷assoc ⟩
            ψ⁰ ⊗₁ f ▷ (ψ-at I B ▷ T₁ (λ-at B)) ▷ T₁ (η-at B) ▷ μ-at B
          ≡⟨ cong (λ x → ψ⁰ ⊗₁ f ▷ x) ▷assoc ⟩
            ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B) ▷ T₁ (η-at B) ▷ μ-at B
          ≡⟨ cong (λ x → ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ x) (sym ▷assoc) ⟩
            ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ (T₁ (λ-at B) ▷ T₁ (η-at B)) ▷ μ-at B
          ≡⟨ cong (λ x → ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ x ▷ μ-at B) (sym TstrictComposition) ⟩
            ψ⁰ ⊗₁ f ▷ ψ-at I B ▷ T₁ (λ-at B ▷ η-at B) ▷ μ-at B
          ≡⟨ sym ▷assoc ⟩
            (ψ⁰ ⊗₁ f ▷ ψ-at I B) ▷ T₁ (λ-at B ▷ η-at B) ▷ μ-at B
          ∎
  in record
    { λ-naturality = λ {A B f} →
      begin
        (λ-at A ▷ η-at A) ▷ T₁ f ▷ μ-at B
      ≡⟨ ▷assoc ⟩
        λ-at A ▷ η-at A ▷ T₁ f ▷ μ-at B
      ≡⟨ cong (λ x → λ-at A ▷ x) 𝕂-▷lunit ⟩
        λ-at A ▷ f
      ≡⟨ t ⟩
        (ψ⁰ ⊗₁ f ▷ ψ-at I B) ▷ T₁ (λ-at B ▷ η-at B) ▷ μ-at B
      ∎
    ; ρ-naturality = λ {A B f} →
      begin
        (ρ-at A ▷ η-at (A ⊗ I)) ▷ T₁ (f ⊗₁ ψ⁰ ▷ ψ-at B I) ▷ μ-at (B ⊗ I)
      ≡⟨ ▷assoc ⟩
        ρ-at A ▷ η-at (A ⊗ I) ▷ T₁ (f ⊗₁ ψ⁰ ▷ ψ-at B I) ▷ μ-at (B ⊗ I)
      ≡⟨ cong (λ x → ρ-at A ▷ x) 𝕂-▷lunit ⟩
        ρ-at A ▷ f ⊗₁ ψ⁰ ▷ ψ-at B I
      ≡⟨ cong (λ x → ρ-at A ▷ x ⊗₁ ψ⁰ ▷ ψ-at B I) ▷runit ⟩
        ρ-at A ▷ (f ▷ id (T B)) ⊗₁ ψ⁰ ▷ ψ-at B I
      ≡⟨ cong (λ x → ρ-at A ▷ (f ▷ id (T B)) ⊗₁ x ▷ ψ-at B I) (sym ▷lunit) ⟩
        ρ-at A ▷ (f ▷ id (T B)) ⊗₁ (id I ▷ ψ⁰) ▷ ψ-at B I
      ≡⟨ cong (λ x → ρ-at A ▷ x ▷ ψ-at B I) MonoidalProduct.strictComposition ⟩
        ρ-at A ▷ (f ⊗₁ id I ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I
      ≡⟨ sym ▷assoc ⟩
        (ρ-at A ▷ f ⊗₁ id I ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I
      ≡⟨ cong (λ x → x ▷ ψ-at B I) (sym ▷assoc) ⟩
        ((ρ-at A ▷ f ⊗₁ id I) ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I
      ≡⟨ cong (λ x → ((ρ-at A ▷ f ⊗₁ x) ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I) (sym funcI.strictIdentity) ⟩
        (((ρ-at A ▷ f ⊗₁ I₁) ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I)
      ≡⟨ cong (λ x → (x ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I) (ℂ.ρ-naturality f) ⟩
        ((f ▷ ρ-at (T B)) ▷ id (T B) ⊗₁ ψ⁰) ▷ ψ-at B I
      ≡⟨ ▷assoc ⟩
        (f ▷ ρ-at (T B)) ▷ id (T B) ⊗₁ ψ⁰ ▷ ψ-at B I
      ≡⟨ ▷assoc ⟩
        f ▷ ρ-at (T B) ▷ id (T B) ⊗₁ ψ⁰ ▷ ψ-at B I
      ≡⟨ cong (λ x → f ▷ x) diagram5 ⟩
        f ▷ T₁ (ρ-at B)
      ≡⟨ ▷runit ⟩
        (f ▷ T₁ (ρ-at B)) ▷ id (T (B ⊗ I))
      ≡⟨ cong (λ x → _ ▷ x) (sym diagram2) ⟩
        (f ▷ T₁ (ρ-at B)) ▷ T₁ (η-at (B ⊗ I)) ▷ μ-at (B ⊗ I)
      ≡⟨ ▷assoc ⟩
        f ▷ T₁ (ρ-at B) ▷ T₁ (η-at (B ⊗ I)) ▷ μ-at (B ⊗ I)
      ≡⟨ cong (λ x → f ▷ x) (sym ▷assoc) ⟩
        f ▷ (T₁ (ρ-at B) ▷ T₁ (η-at (B ⊗ I))) ▷ μ-at (B ⊗ I)
      ≡⟨ cong (λ x → f ▷ x ▷ μ-at _) (sym TstrictComposition) ⟩
        f ▷ T₁ (ρ-at B ▷ η-at (B ⊗ I)) ▷ μ-at (B ⊗ I)
      ∎
      ; α-naturality = λ {A B C X Y Z} {f g h} →
      begin
        ((f ⊗₁ g ▷ ψ-at _ _) ⊗₁ h ▷ ψ-at (_ ⊗ _) _)
          ▷ T₁ (α-at _ _ _ ▷ η-at (_ ⊗ (_ ⊗ _))) ▷ μ-at (_ ⊗ (_ ⊗ _))
      ≡⟨ cong (λ x → ((f ⊗₁ g ▷ ψ-at _ _) ⊗₁ _ ▷ ψ-at _ _) ▷ x ▷ _) TstrictComposition ⟩
        ((f ⊗₁ g ▷ ψ-at _ _) ⊗₁ h ▷ ψ-at (_ ⊗ _) _)
          ▷ (T₁ (α-at _ _ _) ▷ T₁ (η-at (_ ⊗ (_ ⊗ _)))) ▷ μ-at (_ ⊗ (_ ⊗ _))
      ≡⟨ cong (λ x → ((f ⊗₁ g ▷ ψ-at _ _) ⊗₁ h ▷ ψ-at (_ ⊗ _) _) ▷ x) ▷assoc ⟩
        ((f ⊗₁ g ▷ ψ-at _ _) ⊗₁ h ▷ ψ-at (_ ⊗ _) _)
           ▷ T₁ (α-at _ _ _) ▷ T₁ (η-at (_ ⊗ (_ ⊗ _))) ▷ μ-at (_ ⊗ (_ ⊗ _))
      ≡⟨ cong (λ x → (((f ⊗₁ g ▷ ψ-at _ _) ⊗₁ _) ▷ ψ-at (_ ⊗ _) _) ▷ _ ▷ x) diagram2 ⟩
        ((f ⊗₁ g ▷ ψ-at _ _) ⊗₁ h ▷ ψ-at (_ ⊗ _) _) ▷ T₁ (α-at _ _ _) ▷ id (T (_ ⊗ (_ ⊗ _)))
      ≡⟨ cong (λ x → ((f ⊗₁ g ▷ ψ-at _ _) ⊗₁ h ▷ ψ-at _ _) ▷ x) (sym ▷runit) ⟩
        ((f ⊗₁ g ▷ ψ-at _ _) ⊗₁ h ▷ ψ-at (_ ⊗ _) _) ▷ T₁ (α-at _ _ _)
      ≡⟨ cong (λ x → (_ ⊗₁ x ▷ _) ▷ _) ▷runit ⟩
        ((f ⊗₁ g ▷ ψ-at _ _) ⊗₁ (h ▷ id (T _)) ▷ ψ-at (_ ⊗ _) _) ▷ T₁ (α-at _ _ _)
      ≡⟨ cong (λ x → (x ▷ ψ-at (_ ⊗ _) _) ▷ T₁ (α-at _ _ _)) MonoidalProduct.strictComposition ⟩
        (((f ⊗₁ g) ⊗₁ h ▷ ψ-at _ _ ⊗₁ id (T _)) ▷ ψ-at (_ ⊗ _) _) ▷ T₁ (α-at _ _ _)
      ≡⟨ ▷assoc ⟩
        ((f ⊗₁ g) ⊗₁ h ▷ ψ-at _ _ ⊗₁ id (T _)) ▷ ψ-at (_ ⊗ _) _ ▷ T₁ (α-at _ _ _)
      ≡⟨ ▷assoc ⟩
        (f ⊗₁ g) ⊗₁ h ▷ ψ-at _ _ ⊗₁ id (T _) ▷ ψ-at (_ ⊗ _) _ ▷ T₁ (α-at _ _ _)
      ≡⟨ cong (λ x → (f ⊗₁ g) ⊗₁ h ▷ x) (sym diagram6) ⟩
        (f ⊗₁ g) ⊗₁ h ▷ α-at (T _) (T _) (T _) ▷ id (T _) ⊗₁ ψ-at _ _ ▷ ψ-at _ (_ ⊗ _)
      ≡⟨ sym ▷assoc ⟩
        ((f ⊗₁ g) ⊗₁ h ▷ α-at (T _) (T _) (T _)) ▷ id (T _) ⊗₁ ψ-at _ _ ▷ ψ-at _ (_ ⊗ _)
      ≡⟨ cong (λ x → x ▷ id (T _) ⊗₁ ψ-at _ _ ▷ ψ-at _ (_ ⊗ _)) (α-naturality f g h) ⟩
        (α-at A B C ▷ f ⊗₁ (g ⊗₁ h)) ▷ id (T _) ⊗₁ ψ-at _ _ ▷ ψ-at _ (_ ⊗ _)
      ≡⟨ ▷assoc ⟩
        α-at A B C ▷ f ⊗₁ (g ⊗₁ h) ▷ id (T _) ⊗₁ ψ-at _ _ ▷ ψ-at _ (_ ⊗ _)
      ≡⟨ cong (λ x → _ ▷ x) (sym ▷assoc) ⟩
        α-at A B C ▷ (f ⊗₁ (g ⊗₁ h) ▷ id (T _) ⊗₁ ψ-at _ _) ▷ ψ-at _ (_ ⊗ _)
      ≡⟨ cong (λ x → _ ▷ x ▷ ψ-at _ (_ ⊗ _)) (sym MonoidalProduct.strictComposition) ⟩
        α-at A B C ▷ ((f ▷ id (T _)) ⊗₁ (g ⊗₁ h ▷ ψ-at _ _)) ▷ ψ-at _ (_ ⊗ _)
      ≡⟨ cong (λ x → _ ▷ x ⊗₁ _ ▷ _) (sym ▷runit) ⟩
        α-at A B C ▷ f ⊗₁ (g ⊗₁ h ▷ ψ-at _ _) ▷ ψ-at _ (_ ⊗ _)
      ≡⟨ cong (λ x → _ ▷ x) (sym 𝕂-▷lunit) ⟩
        α-at A B C ▷ η-at (A ⊗ (B ⊗ C))
          ▷ T₁ (f ⊗₁ (g ⊗₁ h ▷ ψ-at _ _) ▷ ψ-at _ (_ ⊗ _)) ▷ μ-at (_ ⊗ (_ ⊗ _))
      ≡⟨ sym ▷assoc ⟩
        (α-at A B C ▷ η-at (A ⊗ (B ⊗ C)))
          ▷ T₁ (f ⊗₁ (g ⊗₁ h ▷ ψ-at _ _) ▷ ψ-at _ (_ ⊗ _)) ▷ μ-at (_ ⊗ (_ ⊗ _))
      ∎
    ; ich4a = λ {A} {B} {C} {X} {Y} {Z} {f} {g} {m} {n} →
      begin
        (f ⊗₁ g ▷ η-at (B ⊗ Y)) ▷ T₁ (m ⊗₁ n ▷ ψ-at C Z) ▷ μ-at (C ⊗ Z)
      ≡⟨ ▷assoc ⟩
        f ⊗₁ g ▷ η-at (B ⊗ Y) ▷ T₁ (m ⊗₁ n ▷ ψ-at C Z) ▷ μ-at (C ⊗ Z)
      ≡⟨ cong (λ x → f ⊗₁ g ▷ x) 𝕂-▷lunit ⟩
        f ⊗₁ g ▷ m ⊗₁ n ▷ ψ-at C Z
      ≡⟨ sym ▷assoc ⟩
        (f ⊗₁ g ▷ m ⊗₁ n) ▷ ψ-at C Z
      ≡⟨ cong (λ x → x ▷ ψ-at C Z) (sym MonoidalProduct.strictComposition) ⟩
        (f ▷ m) ⊗₁ (g ▷ n) ▷ ψ-at C Z
      ≡⟨ cong (λ x → (f ▷ x) ⊗₁ (g ▷ n) ▷ ψ-at C Z) (sym 𝕂-▷lunit) ⟩
        (f ▷ η-at B ▷ T₁ m ▷ μ-at C) ⊗₁ (g ▷ n) ▷ ψ-at C Z
      ≡⟨ cong (λ x → (f ▷ η-at B ▷ T₁ m ▷ μ-at C) ⊗₁ (g ▷ x) ▷ ψ-at C Z) (sym 𝕂-▷lunit) ⟩
        (f ▷ η-at B ▷ T₁ m ▷ μ-at C) ⊗₁ (g ▷ η-at Y ▷ T₁ n ▷ μ-at Z) ▷ ψ-at C Z
      ≡⟨ cong (λ x → x ⊗₁ (g ▷ η-at Y ▷ T₁ n ▷ μ-at Z) ▷ ψ-at C Z) (sym ▷assoc) ⟩
        ((f ▷ η-at B) ▷ T₁ m ▷ μ-at C) ⊗₁ (g ▷ η-at Y ▷ T₁ n ▷ μ-at Z) ▷ ψ-at C Z
      ≡⟨ cong (λ x → ((f ▷ η-at B) ▷ T₁ m ▷ μ-at C) ⊗₁ x ▷ ψ-at C Z) (sym ▷assoc) ⟩
        ((f ▷ η-at B) ▷ T₁ m ▷ μ-at C) ⊗₁ ((g ▷ η-at Y) ▷ T₁ n ▷ μ-at Z) ▷ ψ-at C Z
      ∎
    ; ich4b =  λ {A B C X Y Z k ℓ h i} →
      begin
       (k ⊗₁ ℓ ▷ ψ-at B Y) ▷ T₁ (h ⊗₁ i ▷ η-at (C ⊗ Z)) ▷ μ-at (C ⊗ Z)
      ≡⟨ cong (λ x → (k ⊗₁ ℓ ▷ ψ-at B Y) ▷ x ▷ μ-at _) TstrictComposition ⟩
        (k ⊗₁ ℓ ▷ ψ-at B Y) ▷ (T₁ (h ⊗₁ i) ▷ T₁ (η-at (C ⊗ Z))) ▷ μ-at (C ⊗ Z)
      ≡⟨ cong (λ x → (k ⊗₁ ℓ ▷ _) ▷ x) ▷assoc ⟩
        (k ⊗₁ ℓ ▷ ψ-at B Y) ▷ T₁ (h ⊗₁ i) ▷ T₁ (η-at (C ⊗ Z)) ▷ μ-at (C ⊗ Z)
      ≡⟨ cong (λ x → (k ⊗₁ ℓ ▷ _) ▷ T₁ (h ⊗₁ i) ▷ x) diagram2 ⟩
        (k ⊗₁ ℓ ▷ ψ-at B Y) ▷ T₁ (h ⊗₁ i) ▷ id (T (C ⊗ Z))
      ≡⟨ cong (λ x → (k ⊗₁ ℓ ▷ _) ▷ x) (sym ▷runit) ⟩
        (k ⊗₁ ℓ ▷ ψ-at B Y) ▷ T₁ (h ⊗₁ i)
      ≡⟨ ▷assoc ⟩
        k ⊗₁ ℓ ▷ ψ-at B Y ▷ T₁ (h ⊗₁ i)
      ≡⟨ cong (λ x → k ⊗₁ ℓ ▷ x) (sym ψ-naturality) ⟩
        k ⊗₁ ℓ ▷ T₁ h ⊗₁ T₁ i ▷ ψ-at C Z
      ≡⟨ sym ▷assoc ⟩
        (k ⊗₁ ℓ ▷ T₁ h ⊗₁ T₁ i) ▷ ψ-at C Z
      ≡⟨ cong (λ x → x ▷ _) (sym MonoidalProduct.strictComposition) ⟩
        (k ▷ T₁ h) ⊗₁ (ℓ ▷ T₁ i) ▷ ψ-at C Z
      ≡⟨ cong (λ x → (k ▷ x) ⊗₁ (_ ▷ _) ▷ _) ▷runit ⟩
        (k ▷ T₁ h ▷ id (T C)) ⊗₁ (ℓ ▷ T₁ i) ▷ ψ-at C Z
      ≡⟨ cong (λ x → (k ▷ T₁ h ▷ x) ⊗₁ (ℓ ▷ T₁ i) ▷ ψ-at C Z) (sym diagram2)  ⟩
        (k ▷ T₁ h ▷ T₁ (η-at C) ▷ μ-at C) ⊗₁ (ℓ ▷ T₁ i) ▷ ψ-at C Z
      ≡⟨  cong (λ x → (k ▷ x) ⊗₁ (ℓ ▷ T₁ i) ▷ ψ-at C Z) (sym ▷assoc) ⟩
        (k ▷ (T₁ h ▷ T₁ (η-at C)) ▷ μ-at C) ⊗₁ (ℓ ▷ T₁ i) ▷ ψ-at C Z
      ≡⟨ cong (λ x → (k ▷ x ▷ μ-at C) ⊗₁ (ℓ ▷ T₁ i) ▷ ψ-at C Z) (sym TstrictComposition) ⟩
        (k ▷ T₁ (h ▷ η-at C) ▷ μ-at C) ⊗₁ (ℓ ▷ T₁ i) ▷ ψ-at C Z
      ≡⟨ cong (λ x → (_ ▷ T₁ _ ▷ _) ⊗₁ (ℓ ▷ x) ▷ _ ) ▷runit ⟩
        (k ▷ T₁ (h ▷ η-at C) ▷ μ-at C) ⊗₁ (ℓ ▷ T₁ i ▷ id (T Z)) ▷ ψ-at C Z
      ≡⟨ cong (λ x → (k ▷ T₁ _ ▷ μ-at _) ⊗₁ (ℓ ▷ T₁ i ▷ x) ▷ ψ-at C Z) (sym diagram2) ⟩
        (k ▷ T₁ (h ▷ η-at C) ▷ μ-at C) ⊗₁ (ℓ ▷ T₁ i ▷ T₁ (η-at Z) ▷ μ-at Z) ▷ ψ-at C Z
      ≡⟨ cong (λ x → (k ▷ T₁ (h ▷ η-at C) ▷ μ-at C) ⊗₁ (ℓ ▷ x) ▷ ψ-at C Z) (sym ▷assoc) ⟩
        (k ▷ T₁ (h ▷ η-at C) ▷ μ-at C) ⊗₁ (ℓ ▷ (T₁ i ▷ T₁ (η-at Z)) ▷ μ-at Z) ▷ ψ-at C Z
      ≡⟨ cong (λ x → (k ▷ T₁ (h ▷ η-at C) ▷ μ-at C) ⊗₁ (ℓ ▷ x ▷ μ-at Z) ▷ ψ-at C Z) (sym TstrictComposition) ⟩
       (k ▷ T₁ (h ▷ η-at C) ▷ μ-at C) ⊗₁ (ℓ ▷ T₁ (i ▷ η-at Z) ▷ μ-at Z) ▷ ψ-at C Z
      ∎
    }

Kleisli-construction : (ℂ : MonoidalCategory) (T : ConcurrentMonad ℂ) → ConcurrentCategory ℂ
Kleisli-construction ℂ T =
  let open MonoidalCategory ℂ
      open ConcurrentMonad T renaming (F₁ to T₁ ; F₀ to T₀)
  in record
    { 𝕂 = Kleisli-𝕂 ℂ T
    ; J = Kleisli-J ℂ T
    ; isConcurrentCategory = Kleisli-isConcurrentCategory ℂ T
    }

-- examples, right adjoint to J <- ordered adjunction <- natural bijection