{-# OPTIONS --type-in-type --allow-unsolved-metas #-}
open import Base
open import Monoidal
open import Concurrent
open import Kleisli

toCategory : {c : Set} → ParamCategory c → Category
toCategory {c} PC = record { obj = c ; PC = PC }

toFunctor : {c : Set} {P Q : ParamCategory c} {F₀ : c → c} → ParamFunctor P Q F₀ → Functor (toCategory P) (toCategory Q)
toFunctor {c} {P} {Q} {F₀} PF = record { F₀ = F₀ ; PF = PF }

-- this is a special type of adjunction where the left adjoint is identity-on-objects
record AreAdjoint {c : Set} {ℂ : ParamCategory c} {𝔻 : ParamCategory c}
                  (L : ParamFunctor ℂ 𝔻 (λ C → C))
                  (R : Functor (toCategory 𝔻) (toCategory ℂ)) : Set where
  private
    module ℂ = ParamCategory ℂ
    module 𝔻 = ParamCategory 𝔻
  L₀ : c → c
  L₀ = λ C → C
  open ParamFunctor L renaming (F₁ to L₁)
  open Functor R renaming (F₀ to R₀; F₁ to R₁)
  field
    η-at : (C : c) → ℂ.hom C (R₀ (L₀ C))
    η-naturality : {A B : c} {f : ℂ.hom A B} → f ℂ.▷ η-at B ≡ η-at A ℂ.▷ R₁ (L₁ f)
    ε-at : (D : c) → 𝔻.hom (L₀ (R₀ D)) D
    ε-naturality : {A B : c} {f : 𝔻.hom A B} → L₁ (R₁ f) 𝔻.▷ ε-at B ≡ ε-at A 𝔻.▷ f
    zigzag-L : {C : c} → 𝔻.id (L₀ C) ≡ L₁ (η-at C) 𝔻.▷ ε-at (L₀ C)
    zigzag-R : {D : c} → ℂ.id (R₀ D) ≡ η-at (R₀ D) ℂ.▷ R₁ (ε-at D)

Kleisli-K-F : (ℂ : MonoidalCategory) (monT : ConcurrentMonad ℂ)
  → Functor (toCategory (Kleisli-P ℂ monT)) (MonoidalCategory.U ℂ)
Kleisli-K-F ℂ monT =
  let open MonoidalCategory ℂ
      open ConcurrentMonad monT renaming (F₀ to T; F₁ to T₁)
      module monT = ConcurrentMonad monT
  in record
    { F₀ = T
    ; PF = record
      { prefunctor = record
        { F₁ = λ {X} {Y} k → T₁ k ▷ μ-at Y
        ; preserveOrder = λ {X} {Y} {f} {g} fg →
          let open ≤-Reasoning {ℂ} in
            ≤begin
              T₁ f ▷ μ-at Y
            ≤⟨ ▷monot≤ (monT.preserveOrder fg) ≤refl ⟩
              T₁ g ▷ μ-at Y
            ≤∎
        }
      ; isParamFunctor = record
        { strictIdentity = diagram2
        ; strictComposition = λ {X} {Y} {Z} {f} {g} →
          begin
            T₁ (f ▷ T₁ g ▷ μ-at Z) ▷ μ-at Z
          ≡⟨ cong (λ x → x ▷ μ-at Z) monT.strictComposition ⟩
            (T₁ f ▷ T₁ (T₁ g ▷ μ-at Z)) ▷ μ-at Z
          ≡⟨ cong (λ x → (T₁ f ▷ x) ▷ _) monT.strictComposition ⟩
            (T₁ f ▷ T₁ (T₁ g) ▷ T₁ (μ-at Z)) ▷ μ-at Z
          ≡⟨ ▷assoc ⟩
            T₁ f ▷ (T₁ (T₁ g) ▷ T₁ (μ-at Z)) ▷ μ-at Z
          ≡⟨ cong (λ x → T₁ f ▷ x) ▷assoc ⟩
            T₁ f ▷ T₁ (T₁ g) ▷ T₁ (μ-at Z) ▷ μ-at Z
          ≡⟨ cong (λ x → T₁ f ▷ T₁ (T₁ g) ▷ x) diagram3 ⟩
            T₁ f ▷ T₁ (T₁ g) ▷ μ-at (T Z) ▷ μ-at Z
          ≡⟨ cong (λ x → T₁ f ▷ x) (sym ▷assoc) ⟩
            T₁ f ▷ (T₁ (T₁ g) ▷ μ-at (T Z)) ▷ μ-at Z
          ≡⟨ cong (λ x → T₁ f ▷ x ▷ _) μ-naturality ⟩
            T₁ f ▷ (μ-at Y ▷ T₁ g) ▷ μ-at Z
          ≡⟨ cong (λ x → T₁ f ▷ x) ▷assoc ⟩
            (T₁ f ▷ μ-at Y ▷ T₁ g ▷ μ-at Z)
          ≡⟨ sym ▷assoc ⟩
            (T₁ f ▷ μ-at Y) ▷ T₁ g ▷ μ-at Z
          ∎
        }
      }
    }

Kleisli-K-isLaxMonoidalFunctor : (ℂ : MonoidalCategory) (T : ConcurrentMonad ℂ)
  → IsKLaxMonoidalFunctor {_} {_} {_} {Kleisli-𝕂 ℂ T} {MonoidalCategory.P-monoidal ℂ} (JFunctor.F (Kleisli-J ℂ T)) (Kleisli-K-F ℂ T)
Kleisli-K-isLaxMonoidalFunctor ℂ monT =
  let open MonoidalCategory ℂ
      open ConcurrentMonad monT renaming (F₁ to T₁ ; F₀ to T)
      module monT = ConcurrentMonad monT
  in record
    { ϕ-at = ψ-at
    ; ϕ-naturality = λ {A} {B} {C} {D} {f} {g} →
      let open ≤-Reasoning {ℂ} in
      ≤begin
        ψ-at A C ▷ T₁ (f ⊗₁ g ▷ ψ-at B D) ▷ μ-at (B ⊗ D)
      ≦⟨ cong (λ x → _ ▷ x ▷ _) monT.strictComposition ⟩
        ψ-at A C ▷ (T₁ (f ⊗₁ g) ▷ (T₁ (ψ-at B D))) ▷ μ-at (B ⊗ D)
      ≦⟨ cong (λ x → _ ▷ x) ▷assoc ⟩
        ψ-at A C ▷ T₁ (f ⊗₁ g) ▷ T₁ (ψ-at B D) ▷ μ-at (B ⊗ D)
      ≦⟨ sym ▷assoc ⟩
        (ψ-at A C ▷ T₁ (f ⊗₁ g)) ▷ T₁ (ψ-at B D) ▷ μ-at (B ⊗ D)
      ≦⟨ cong (λ x → x ▷ T₁ _ ▷ μ-at _) (sym ψ-naturality) ⟩
        (T₁ f ⊗₁ T₁ g ▷ ψ-at (T B) (T D)) ▷ T₁ (ψ-at B D) ▷ μ-at (B ⊗ D)
      ≦⟨ ▷assoc ⟩
        T₁ f ⊗₁ T₁ g ▷ ψ-at (T B) (T D) ▷ T₁ (ψ-at B D) ▷ μ-at (B ⊗ D)
      ≤⟨ ▷monot≤ ≤refl inequation4 ⟩
        T₁ f ⊗₁ T₁ g ▷ μ-at B ⊗₁ μ-at D ▷ ψ-at B D
      ≦⟨ sym ▷assoc ⟩
        (T₁ f ⊗₁ T₁ g ▷ μ-at B ⊗₁ μ-at D) ▷ ψ-at B D
      ≦⟨ cong (λ x → x ▷ _) (sym MonoidalProduct.strictComposition) ⟩
        (T₁ f ▷ μ-at B) ⊗₁ (T₁ g ▷ μ-at D) ▷ ψ-at B D
      ≤∎
    ; ϕ⁰ = ψ⁰
    ; laxAssoc = λ {X} {Y} {Z} →
      begin
        ψ-at X Y ⊗₁ id (T Z) ▷ ψ-at (X ⊗ Y) Z ▷ T₁ (α-at X Y Z ▷ η-at (X ⊗ Y ⊗ Z))
          ▷ μ-at (X ⊗ Y ⊗ Z)
      ≡⟨ cong (λ x → (ψ-at X Y ⊗₁ id (T Z)) ▷ _ ▷ x ▷ _) monT.strictComposition ⟩
        ψ-at X Y ⊗₁ id (T Z) ▷ ψ-at (X ⊗ Y) Z ▷ (T₁ (α-at X Y Z) ▷ T₁ (η-at (X ⊗ Y ⊗ Z)))
          ▷ μ-at (X ⊗ Y ⊗ Z)
      ≡⟨ cong (λ x → ψ-at X Y ⊗₁ id (T Z) ▷ ψ-at (X ⊗ Y) Z ▷ x) ▷assoc ⟩
        ψ-at X Y ⊗₁ id (T Z) ▷ ψ-at (X ⊗ Y) Z ▷ T₁ (α-at X Y Z) ▷ T₁ (η-at (X ⊗ Y ⊗ Z))
          ▷ μ-at (X ⊗ Y ⊗ Z)
      ≡⟨ cong (λ x → ψ-at X Y ⊗₁ id (T Z) ▷ ψ-at (X ⊗ Y) Z ▷ _ ▷ x) diagram2 ⟩
        ψ-at X Y ⊗₁ id (T Z) ▷ ψ-at (X ⊗ Y) Z ▷ T₁ (α-at X Y Z) ▷ id (T (X ⊗ Y ⊗ Z))
      ≡⟨ cong (λ x → ψ-at X Y ⊗₁ id (T Z) ▷ _ ▷ x) (sym ▷runit) ⟩
        ψ-at X Y ⊗₁ id (T Z) ▷ ψ-at (X ⊗ Y) Z ▷ T₁ (α-at X Y Z)
      ≡⟨ sym diagram6 ⟩
        α-at (T X) (T Y) (T Z) ▷ id (T X) ⊗₁ ψ-at Y Z ▷ ψ-at X (Y ⊗ Z)
      ∎
    ; laxLunital = λ {X} →
      begin
         λ-at (T X)
      ≡⟨ diagram4 ⟩
        ψ⁰ ⊗₁ id (T X) ▷ ψ-at I X ▷ T₁ (λ-at X)
      ≡⟨ cong (λ x → ψ⁰ ⊗₁ id (T X) ▷ _ ▷ x) ▷runit ⟩
        ψ⁰ ⊗₁ id (T X) ▷ ψ-at I X ▷ T₁ (λ-at X) ▷ id (T X)
      ≡⟨ cong (λ x → ψ⁰ ⊗₁ id (T X) ▷ ψ-at I X ▷ T₁ (λ-at X) ▷ x) (sym diagram2) ⟩
        ψ⁰ ⊗₁ id (T X) ▷ ψ-at I X ▷ T₁ (λ-at X) ▷ T₁ (η-at X) ▷ μ-at X
      ≡⟨ cong (λ x → (_ ⊗₁ id _) ▷ ψ-at I X ▷ x) (sym ▷assoc) ⟩
        ψ⁰ ⊗₁ id (T X) ▷ ψ-at I X ▷ (T₁ (λ-at X) ▷ T₁ (η-at X)) ▷ μ-at X
      ≡⟨ cong (λ x → ψ⁰ ⊗₁ id (T X) ▷ _ ▷ x ▷ _) (sym monT.strictComposition) ⟩
        ψ⁰ ⊗₁ id (T X) ▷ ψ-at I X ▷ T₁ (λ-at X ▷ η-at X) ▷ μ-at X
      ∎
    ; laxRunital = λ {X} → 
      begin
        T₁ (ρ-at X ▷ η-at (X ⊗ I)) ▷ μ-at (X ⊗ I)
      ≡⟨ cong (λ x → x ▷ _) (monT.strictComposition) ⟩
        (T₁ (ρ-at X) ▷ T₁ (η-at (X ⊗ I))) ▷ μ-at (X ⊗ I)
      ≡⟨ ▷assoc ⟩
        T₁ (ρ-at X) ▷ T₁ (η-at (X ⊗ I)) ▷ μ-at (X ⊗ I)
      ≡⟨ cong (λ x → _ ▷ x) diagram2 ⟩
        T₁ (ρ-at X) ▷ id (T (X ⊗ I))
      ≡⟨ sym ▷runit ⟩
        T₁ (ρ-at X)
      ≡⟨ sym diagram5 ⟩
        ρ-at (T X) ▷ id (T X) ⊗₁ ψ⁰ ▷ ψ-at X I
      ∎
    ; preserveI₁ = let open ≤-Reasoning {ℂ} in
      ≤begin
        ψ⁰ ▷ T₁ ψ⁰ ▷ μ-at I
      ≤⟨ inequation2 ⟩
        ψ⁰
      ≦⟨ sym ▷lunit ⟩
        id I ▷ ψ⁰
      ≦⟨ cong (λ x → x ▷ ψ⁰) (sym funcI.strictIdentity) ⟩
        I₁ ▷ ψ⁰
      ≤∎
    ; preserve⊗₁ = λ {X} {Y} {U} {V} {f} {g} → let open ≤-Reasoning {ℂ} in
      ≤begin
        ψ-at X U ▷ T₁ (f ⊗₁ g ▷ ψ-at Y V) ▷ μ-at (Y ⊗ V)
      ≦⟨ cong (λ x → _ ▷ x ▷ _) monT.strictComposition ⟩
         ψ-at X U ▷ (T₁ (f ⊗₁ g) ▷ T₁ (ψ-at Y V)) ▷ μ-at (Y ⊗ V)
      ≦⟨ sym ▷assoc ⟩
         (ψ-at X U ▷ T₁ (f ⊗₁ g) ▷ T₁ (ψ-at Y V)) ▷ μ-at (Y ⊗ V)
      ≦⟨ cong (λ x → x ▷ μ-at (Y ⊗ V)) (sym ▷assoc) ⟩
        ((ψ-at X U ▷ T₁ (f ⊗₁ g)) ▷ T₁ (ψ-at Y V)) ▷ μ-at (Y ⊗ V)
      ≦⟨ cong (λ x → (x ▷ T₁ (ψ-at Y V)) ▷ μ-at (Y ⊗ V)) (sym ψ-naturality) ⟩
        ((T₁ f ⊗₁ T₁ g ▷ ψ-at (T Y) (T V)) ▷ T₁ (ψ-at Y V)) ▷ μ-at (Y ⊗ V)
      ≦⟨ ▷assoc ⟩
        (T₁ f ⊗₁ T₁ g ▷ ψ-at (T Y) (T V)) ▷ T₁ (ψ-at Y V) ▷ μ-at (Y ⊗ V)
      ≦⟨ ▷assoc ⟩
        T₁ f ⊗₁ T₁ g ▷ ψ-at (T Y) (T V) ▷ T₁ (ψ-at Y V) ▷ μ-at (Y ⊗ V)
      ≤⟨ ▷monot≤ ≤refl inequation4 ⟩
        T₁ f ⊗₁ T₁ g ▷ μ-at Y ⊗₁ μ-at V ▷ ψ-at Y V
      ≦⟨ sym ▷assoc ⟩
        (T₁ f ⊗₁ T₁ g ▷ μ-at Y ⊗₁ μ-at V) ▷ ψ-at Y V
      ≦⟨ cong (λ x → x ▷ ψ-at Y V) (sym MonoidalProduct.strictComposition) ⟩
        (T₁ f ▷ μ-at Y) ⊗₁ (T₁ g ▷ μ-at V) ▷ ψ-at Y V
      ≤∎
    }

Kleisli-K : (ℂ : MonoidalCategory) (monT : ConcurrentMonad ℂ)
                       → KFunctor (Kleisli-𝕂 ℂ monT) (MonoidalCategory.P-monoidal ℂ) (Kleisli-J ℂ monT)
Kleisli-K ℂ monT =
  record
    { F = Kleisli-K-F ℂ monT
    ; isKLaxMonoidalFunctor = Kleisli-K-isLaxMonoidalFunctor ℂ monT
    }                       

JK-adjunction : (ℂ : MonoidalCategory) (monT : ConcurrentMonad ℂ)
  → AreAdjoint (JFunctor.F (Kleisli-J ℂ monT))
               (KFunctor.F (Kleisli-K ℂ monT))
JK-adjunction ℂ monT =
  let open MonoidalCategory ℂ
      open ConcurrentMonad monT renaming (F₀ to T; F₁ to T₁)
      𝕂-▷lunit = ParamCategory.▷lunit (Kleisli-P ℂ monT)
  in record
    { η-at = η-at
    ; η-naturality = λ {A B f} → sym 𝕂-▷lunit
    ; ε-at = λ x → id (T x)
    ; ε-naturality = λ {A B f} →
      begin
        ((T₁ f ▷ μ-at B) ▷ η-at (T B)) ▷ T₁ (id (T B)) ▷ μ-at B
      ≡⟨ ▷assoc ⟩
        (T₁ f ▷ μ-at B) ▷ η-at (T B) ▷ T₁ (id (T B)) ▷ μ-at B
      ≡⟨ cong (λ x → (T₁ f ▷ μ-at B) ▷ x) 𝕂-▷lunit ⟩
        (T₁ f ▷ μ-at B) ▷ id (T B)
      ≡⟨ sym ▷runit ⟩
        T₁ f ▷ μ-at B
      ≡⟨ sym ▷lunit ⟩
        id (T A) ▷ T₁ f ▷ μ-at B
      ∎
    ; zigzag-L = λ {D} →
      begin
        η-at D
      ≡⟨ ▷runit ⟩
        η-at D ▷ id (T D)
      ≡⟨ cong (λ x → _ ▷ x) (sym 𝕂-▷lunit) ⟩
        η-at D ▷ η-at (T D) ▷ T₁ (id (T D)) ▷ μ-at D
      ≡⟨ sym ▷assoc ⟩
        (η-at D ▷ η-at (T D)) ▷ T₁ (id (T D)) ▷ μ-at D
      ∎
    ; zigzag-R = sym 𝕂-▷lunit
    }

_▶_ : {𝕏 𝕐 ℤ : Category} → Functor 𝕏 𝕐 → Functor 𝕐 ℤ → Functor 𝕏 ℤ
_▶_ {𝕏} {𝕐} {ℤ} V W = let
    module V = Functor V
    module W = Functor W
    module ℤ = Category ℤ
    module 𝕐 = Category 𝕐
    module 𝕏 = Category 𝕏
    open Functor V renaming (F₀ to V₀; F₁ to V₁)
    open Functor W renaming (F₀ to W₀; F₁ to W₁)
  in record
    { F₀ = λ x → W₀ (V₀ x)
    ; PF = record
      { prefunctor = record
        { F₁ = λ f → W₁ (V₁ f)
        ; preserveOrder = λ {X Y f g} fg → W.preserveOrder (V.preserveOrder fg)
        }
      ; isParamFunctor = record
        { strictIdentity = λ {X} → trans (cong (W₁) V.strictIdentity) W.strictIdentity
        ; strictComposition = λ {_ _ _ f g} →
          begin
            W₁ (V₁ (f 𝕏.▷ g))
          ≡⟨ cong W₁ V.strictComposition ⟩
            W₁ (V₁ f 𝕐.▷ V₁ g)
          ≡⟨ W.strictComposition ⟩
            (W₁ (V₁ f) ℤ.▷ W₁ (V₁ g))
          ∎
        }
      }
    }

-- anything that is the "same operation" in a different context uses dot-notation: eg ℂ.▷ vs 𝕂.▷
-- anything that is unique to one type of structure or is actually the same operation
-- does not: eg ∥ for monoidal-like product which only makes sense in 𝕂 or for tensor on objects

ConcCategoryToConcMonad : (ℂ : MonoidalCategory)
                          (ℍ : ConcurrentCategory ℂ)
                          (K : KFunctor (ConcurrentCategory.𝕂 ℍ) (MonoidalCategory.P-monoidal ℂ) (ConcurrentCategory.J ℍ))
                          (adjunction : AreAdjoint (JFunctor.F (ConcurrentCategory.J ℍ)) (KFunctor.F K))
                          → IsConcurrentMonad {ℂ}
                            ((toFunctor (JFunctor.F (ConcurrentCategory.J ℍ))) ▶ (KFunctor.F K))
ConcCategoryToConcMonad ℂ ℍ K adjunction =
  let
    module ℍ = ConcurrentCategory ℍ
    open AreAdjoint adjunction 
    module K = KFunctor K
    module J = JFunctor (ConcurrentCategory.J ℍ)
    open KFunctor K renaming (F₀ to K₀; F₁ to K₁) hiding (preserveOrder; F; strictIdentity)
    open ParamFunctor J.F renaming (F₁ to J₁) hiding ()
    module ℂ = MonoidalCategory ℂ
    -- would be nice to only have name for the shared object set of ℂ and 𝕂
    open MonoidalCategory ℂ using (I; _⊗_; _⊗₁_)
    module 𝕂 = ParamMonoidalLikeCategory (ConcurrentCategory.𝕂 ℍ)
    open ParamMonoidalLikeCategory (ConcurrentCategory.𝕂 ℍ) using (jd; _∥_)
    J₀ : ℂ.obj → ℂ.obj
    J₀ X = X
    infixr  _♯
    infixr  _♭
    _♯ : {A B : 𝕂.obj} (k : 𝕂.hom A B) → ℂ.hom A (K₀ B)
    _♯ {A} {B} k = η-at A ℂ.▷ K₁ k
    _♭ : {X Y : ℂ.obj} (k : ℂ.hom X (K₀ Y)) → 𝕂.hom X Y
    _♭ {X} {Y} k =  J₁ k 𝕂.▷ ε-at Y
    ♯♭-bijection : {A B : 𝕂.obj} {f : 𝕂.hom A B} → (f ♯)♭ ≡ f
    ♯♭-bijection = λ {A B f} → begin
      J₁ (η-at A ℂ.▷ K₁ f) 𝕂.▷ ε-at B ≡⟨ cong (λ x  → x 𝕂.▷ _) J.strictComposition ⟩
      (J₁ (η-at A) 𝕂.▷ J₁ (K₁ f)) 𝕂.▷ ε-at B ≡⟨ 𝕂.▷assoc ⟩
      J₁ (η-at A) 𝕂.▷ J₁ (K₁ f) 𝕂.▷ ε-at B ≡⟨ cong (λ x → _ 𝕂.▷ x) ε-naturality ⟩
      J₁ (η-at A) 𝕂.▷ ε-at A 𝕂.▷ f ≡⟨ sym 𝕂.▷assoc ⟩
      (J₁ (η-at A) 𝕂.▷ ε-at A) 𝕂.▷ f  ≡⟨ cong (λ x → x 𝕂.▷ f) (sym zigzag-L) ⟩
      𝕂.id A 𝕂.▷ f ≡⟨ 𝕂.▷lunit ⟩
      f ∎
    lemma1 : {A B C : ℂ.obj} {f : ℂ.hom A B} {k : 𝕂.hom B C} → f ℂ.▷ k ♯ ≡ (J₁ f 𝕂.▷ k) ♯
    lemma1 = λ {A B C f k} → begin
      f ℂ.▷ η-at B ℂ.▷ K₁ k           ≡⟨ sym ℂ.▷assoc ⟩
     (f ℂ.▷ η-at B) ℂ.▷ K₁ k          ≡⟨ cong (λ x → x ℂ.▷ K₁ k) η-naturality ⟩
      (η-at A ℂ.▷ K₁ (J₁ f)) ℂ.▷ K₁ k ≡⟨ ℂ.▷assoc ⟩
      η-at A ℂ.▷ K₁ (J₁ f) ℂ.▷ K₁ k   ≡⟨ cong (λ x → η-at A ℂ.▷ x) (sym K.strictComposition) ⟩
      η-at A ℂ.▷ K₁ (J₁ f 𝕂.▷ k)      ∎
    lemma2 : {A B C : ℂ.obj} {f : ℂ.hom B C} {k : 𝕂.hom A B} → (k 𝕂.▷ J₁ f) ♯ ≡ k ♯ ℂ.▷ K₁ (J₁ f)
    lemma2 = λ {A B C f k} → trans (cong (λ x → η-at A ℂ.▷ x) K.strictComposition) (sym ℂ.▷assoc)
    psi-lemma : {A B C D : 𝕂.obj} {k : 𝕂.hom A B} {ℓ : 𝕂.hom C D} → (k ∥ ℓ)♯ ≡ (k ♯ ⊗₁ ℓ ♯) ℂ.▷ (ε-at B ∥ ε-at D) ♯
    psi-lemma = λ {A B C D k ℓ} → begin
      (k ∥ ℓ) ♯ ≡⟨ cong (λ x → (x ∥ ℓ)♯) (sym ♯♭-bijection) ⟩
      ((J₁ (η-at A ℂ.▷ K₁ k) 𝕂.▷ ε-at B) ∥ ℓ) ♯ ≡⟨ cong (λ x → (_ ∥ x)♯) (sym ♯♭-bijection) ⟩
      ((J₁ (η-at A ℂ.▷ K₁ k) 𝕂.▷ ε-at B) ∥ (J₁ (η-at C ℂ.▷ K₁ ℓ) 𝕂.▷ ε-at D)) ♯ ≡⟨ cong _♯ (sym ℍ.ich4a) ⟩
       (J₁ ((η-at A ℂ.▷ K₁ k) ⊗₁ (η-at C ℂ.▷ K₁ ℓ)) 𝕂.▷ ε-at B ∥ ε-at D) ♯ ≡⟨ sym lemma1 ⟩
      (η-at A ℂ.▷ K₁ k) ⊗₁ (η-at C ℂ.▷ K₁ ℓ) ℂ.▷
       η-at (K₀ B ⊗ K₀ D) ℂ.▷ K₁ (ε-at B ∥ ε-at D) ∎
    mi-lemma : {A B C : 𝕂.obj} {k : 𝕂.hom A B} {ℓ : 𝕂.hom B C} → (k 𝕂.▷ ℓ)♯ ≡ k ♯ ℂ.▷ K₁ (J₁ (ℓ ♯)) ℂ.▷ K₁ (ε-at C)
    mi-lemma = λ {A B C k ℓ} → begin
       (k 𝕂.▷ ℓ)♯
     ≡⟨ cong (λ x → η-at A ℂ.▷ x) K.strictComposition ⟩
       η-at A ℂ.▷ K₁ k ℂ.▷ K₁ ℓ
     ≡⟨ cong (λ x → η-at A ℂ.▷ K₁ k ℂ.▷ K₁ x) (sym 𝕂.▷lunit) ⟩
       η-at A ℂ.▷ K₁ k ℂ.▷ K₁ (𝕂.id B 𝕂.▷ ℓ)
     ≡⟨ cong (λ x → η-at A ℂ.▷ K₁ k ℂ.▷ K₁ (x 𝕂.▷ ℓ)) zigzag-L ⟩
       η-at A ℂ.▷ K₁ k ℂ.▷ K₁ ((J₁ (η-at B) 𝕂.▷ ε-at B) 𝕂.▷ ℓ)
     ≡⟨  cong (λ x → η-at A ℂ.▷ K₁ k ℂ.▷ K₁ x) 𝕂.▷assoc ⟩
       η-at A ℂ.▷ K₁ k ℂ.▷ K₁ (J₁ (η-at B) 𝕂.▷ ε-at B 𝕂.▷ ℓ)
     ≡⟨  cong (λ x → η-at A ℂ.▷ K₁ k ℂ.▷ K₁ (J₁ (η-at B) 𝕂.▷ x)) (sym ε-naturality) ⟩
       η-at A ℂ.▷ K₁ k ℂ.▷ K₁ (J₁ (η-at B) 𝕂.▷ J₁ (K₁ ℓ) 𝕂.▷ ε-at C)
     ≡⟨ cong (λ x → η-at A ℂ.▷ K₁ k ℂ.▷ K₁ x) (sym 𝕂.▷assoc) ⟩
       η-at A ℂ.▷ K₁ k ℂ.▷ K₁ ((J₁ (η-at B) 𝕂.▷ J₁ (K₁ ℓ)) 𝕂.▷ ε-at C)
     ≡⟨ cong (λ x → η-at A ℂ.▷ K₁ k ℂ.▷ x) K.strictComposition ⟩
       η-at A ℂ.▷ K₁ k ℂ.▷ K₁ (J₁ (η-at B) 𝕂.▷ J₁ (K₁ ℓ)) ℂ.▷ (K₁ (ε-at C))
     ≡⟨ sym ℂ.▷assoc ⟩
       (η-at A ℂ.▷ K₁ k) ℂ.▷ K₁ (J₁ (η-at B) 𝕂.▷ J₁ (K₁ ℓ)) ℂ.▷ K₁ (ε-at C)
     ≡⟨ cong (λ x → k ♯ ℂ.▷ K₁ x ℂ.▷ K₁ (ε-at C)) (sym J.strictComposition) ⟩
       k ♯ ℂ.▷ K₁ (J₁ (ℓ ♯)) ℂ.▷ K₁ (ε-at C)
     ∎
  in record
    { η-at = λ A → η-at A
    ; η-naturality = λ {A B f} → η-naturality
    ; μ-at = λ A →  K₁ (ε-at A)
    ; μ-naturality = λ {A B f} →
      begin
        K₁ (J₁ (K₁ (J₁ f))) ℂ.▷ K₁ (ε-at B)
      ≡⟨ sym K.strictComposition ⟩
        K₁ (J₁ (K₁ (J₁ f)) 𝕂.▷ ε-at B)
      ≡⟨ cong K₁ ε-naturality ⟩
        K₁ (ε-at A 𝕂.▷ J₁ f)
      ≡⟨ K.strictComposition ⟩
        K₁ (ε-at A) ℂ.▷ K₁ (J₁ f)
      ∎
    ; ψ⁰ = jd ♯
    ; ψ-at = λ A B → (ε-at A ∥ ε-at B)♯
    ; ψ-naturality = λ {A B C D f g} →
      begin
        K₁ (J₁ f) ⊗₁ K₁ (J₁ g) ℂ.▷ η-at (K₀ B ⊗ K₀ D) ℂ.▷ K₁ (ε-at B ∥ ε-at D)
      ≡⟨ lemma1 ⟩
        η-at (K₀ A ⊗ K₀ C) ℂ.▷ K₁ (J₁ (K₁ (J₁ f) ⊗₁ K₁ (J₁ g)) 𝕂.▷ ε-at B ∥ ε-at D)
      ≡⟨ cong _♯ ℍ.ich4a ⟩
        η-at (K₀ A ⊗ K₀ C) ℂ.▷ K₁ ((J₁ (K₁ (J₁ f)) 𝕂.▷ ε-at B) ∥ (J₁ (K₁ (J₁ g)) 𝕂.▷ ε-at D))
      ≡⟨ cong (λ x → (x ∥ (J₁ (K₁ (J₁ g)) 𝕂.▷ ε-at D))♯) ε-naturality ⟩ 
        η-at (K₀ A ⊗ K₀ C) ℂ.▷ K₁ ((ε-at A 𝕂.▷ J₁ f) ∥ (J₁ (K₁ (J₁ g)) 𝕂.▷ ε-at D))
      ≡⟨ cong (λ x → ((ε-at A 𝕂.▷ J₁ f) ∥ x)♯) ε-naturality ⟩
        η-at (K₀ A ⊗ K₀ C) ℂ.▷ K₁ ((ε-at A 𝕂.▷ J₁ f) ∥ (ε-at C 𝕂.▷ J₁ g))
      ≡⟨ cong _♯ (sym ℍ.ich4b) ⟩
        η-at (K₀ A ⊗ K₀ C) ℂ.▷ K₁ ((ε-at A ∥ ε-at C) 𝕂.▷ J₁ (f ⊗₁ g))
      ≡⟨ cong (λ x → _ ℂ.▷ x) K.strictComposition ⟩
        η-at (K₀ A ⊗ K₀ C) ℂ.▷ K₁ (ε-at A ∥ ε-at C) ℂ.▷ K₁ (J₁ (f ⊗₁ g))
      ≡⟨ sym ℂ.▷assoc ⟩
        (η-at (K₀ A ⊗ K₀ C) ℂ.▷ K₁ (ε-at A ∥ ε-at C)) ℂ.▷ K₁ (J₁ (f ⊗₁ g))
      ∎
    ; diagram1 = sym zigzag-R
    ; diagram2 = λ {X} →
      begin
        K₁ (J₁ (η-at X)) ℂ.▷ K₁ (ε-at X)
      ≡⟨ sym K.strictComposition ⟩
        K₁ (J₁ (η-at X) 𝕂.▷ ε-at X)
      ≡⟨ cong K₁ (sym zigzag-L) ⟩
        K₁ (𝕂.id X)
      ≡⟨ K.strictIdentity ⟩
        ℂ.id (K₀ X)  
      ∎
    ; diagram3 = λ {X} →
      begin
        K₁ (J₁ (K₁ (ε-at X))) ℂ.▷ K₁ (ε-at X)
      ≡⟨ sym K.strictComposition ⟩
        K₁ (J₁ (K₁ (ε-at X)) 𝕂.▷ ε-at X)
      ≡⟨ cong K₁ ε-naturality ⟩
        K₁ (ε-at (K₀ X) 𝕂.▷ ε-at X)
      ≡⟨ K.strictComposition ⟩
        K₁ (ε-at (K₀ X)) ℂ.▷ K₁ (ε-at X)
      ∎
    ; diagram4 = λ {X} →
      begin
        ℂ.λ-at (K₀ X)
      ≡⟨ ℂ.▷runit ⟩
        ℂ.λ-at (K₀ X) ℂ.▷ ℂ.id (K₀ X)
      ≡⟨ cong (λ x → ℂ.λ-at _ ℂ.▷ x) zigzag-R ⟩
        ℂ.λ-at (K₀ X) ℂ.▷ η-at (K₀ X) ℂ.▷ K₁ (ε-at X)
      ≡⟨ lemma1 ⟩
        η-at (I ⊗ K₀ X)
        ℂ.▷ K₁ (J₁ (ℂ.λ-at (K₀ X)) 𝕂.▷ ε-at X)
      ≡⟨ cong (λ x → (x 𝕂.▷ _)♯) (refl)  ⟩
        η-at (I ⊗ K₀ X)
        ℂ.▷ K₁ (J₁ (ℂ.λ-at (K₀ X)) 𝕂.▷ ε-at X)
      ≡⟨ cong _♯ ℍ.λ-naturality ⟩
        η-at (I ⊗ K₀ X)
        ℂ.▷ K₁ (jd ∥ ε-at X
          𝕂.▷ J₁ (ℂ.λ-at X))
      ≡⟨ cong (λ x → (x ∥ _ 𝕂.▷ _)♯) (sym ♯♭-bijection) ⟩
        η-at (I ⊗ K₀ X)
        ℂ.▷ K₁ ((J₁ (η-at I ℂ.▷ K₁ jd)
          𝕂.▷ ε-at I) ∥ ε-at X
          𝕂.▷ J₁ (ℂ.λ-at X))
      ≡⟨ cong (λ x → ((J₁ (η-at I ℂ.▷ K₁ jd) 𝕂.▷ ε-at I) ∥ x 𝕂.▷ J₁ (ℂ.λ-at X))♯) (sym 𝕂.▷lunit) ⟩
        η-at (I ⊗ K₀ X)
        ℂ.▷ K₁ ((J₁ (η-at I ℂ.▷ K₁ jd)
          𝕂.▷ ε-at I) ∥ (𝕂.id (K₀ X)
          𝕂.▷ ε-at X)
          𝕂.▷ J₁ (ℂ.λ-at X))
      ≡⟨ cong (λ x → ((J₁ (η-at I ℂ.▷ K₁ jd) 𝕂.▷ ε-at I)
                 ∥ (x 𝕂.▷ ε-at X) 𝕂.▷ J₁ (ℂ.λ-at X))♯) (sym J.strictIdentity) ⟩
        η-at (I ⊗ K₀ X)
        ℂ.▷ K₁ ((J₁ (η-at I ℂ.▷ K₁ jd)
          𝕂.▷ ε-at I) ∥ (J₁ (ℂ.id (K₀ X))
          𝕂.▷ ε-at X)
          𝕂.▷ J₁ (ℂ.λ-at X))
      ≡⟨ cong (λ x → (x 𝕂.▷ J₁ (ℂ.λ-at X)) ♯) (sym ℍ.ich4a) ⟩
        η-at (I ⊗ K₀ X) ℂ.▷
         K₁ ((J₁ ((η-at I ℂ.▷ K₁ jd) ⊗₁ ℂ.id (K₀ X))
         𝕂.▷ ε-at I ∥ ε-at X) 𝕂.▷ J₁ (ℂ.λ-at X))
      ≡⟨ cong (λ x → x ♯) 𝕂.▷assoc ⟩
        η-at (I ⊗ K₀ X) ℂ.▷
         K₁ (J₁ ((η-at I ℂ.▷ K₁ jd) ⊗₁ ℂ.id (K₀ X))
         𝕂.▷ ε-at I ∥ ε-at X 𝕂.▷ J₁ (ℂ.λ-at X))
      ≡⟨ sym lemma1 ⟩
        (η-at I ℂ.▷ K₁ jd) ⊗₁ ℂ.id (K₀ X)
        ℂ.▷  η-at (K₀ I ⊗ K₀ X)
        ℂ.▷ K₁ (ε-at I ∥ ε-at X 𝕂.▷ J₁ (ℂ.λ-at X))
      ≡⟨ cong (λ x → (η-at I ℂ.▷ K₁ jd) ⊗₁ ℂ.id (K₀ X) ℂ.▷ _ ℂ.▷ K₁ (_ ∥ _ 𝕂.▷ x)) (refl) ⟩
        (η-at I ℂ.▷ K₁ jd) ⊗₁ ℂ.id (K₀ X) ℂ.▷
         η-at (K₀ I ⊗ K₀ X) ℂ.▷
         K₁ (ε-at I ∥ ε-at X 𝕂.▷ J₁ (ℂ.λ-at X))
      ≡⟨ cong (λ x → (η-at I ℂ.▷ K₁ jd) ⊗₁ ℂ.id (K₀ X) ℂ.▷ _ ℂ.▷ x) K.strictComposition ⟩
        (η-at I ℂ.▷ K₁ jd) ⊗₁ ℂ.id (K₀ X)
        ℂ.▷ η-at (K₀ I ⊗ K₀ X)
        ℂ.▷ K₁ (ε-at I ∥ ε-at X)
        ℂ.▷ K₁ (J₁ (ℂ.λ-at X))
      ≡⟨ cong (λ x → (η-at I ℂ.▷ K₁ jd) ⊗₁ ℂ.id (K₀ X) ℂ.▷ x) (sym ℂ.▷assoc) ⟩
        (η-at I ℂ.▷ K₁ jd) ⊗₁ ℂ.id (K₀ X)
        ℂ.▷ (η-at (K₀ I ⊗ K₀ X)
        ℂ.▷ K₁ (ε-at I ∥ ε-at X))
        ℂ.▷ K₁ (J₁ (ℂ.λ-at X))
      ∎
    ; diagram5 = λ {X} →
      begin
        ℂ.ρ-at (K₀ X)
        ℂ.▷ ℂ.id (K₀ X) ⊗₁ (η-at I ℂ.▷ K₁ jd)
        ℂ.▷ η-at (K₀ X ⊗ K₀ I)
        ℂ.▷ K₁ (ε-at X ∥ ε-at I)
      ≡⟨ cong (λ x → _ ℂ.▷ x) lemma1 ⟩
        ℂ.ρ-at (K₀ X)
        ℂ.▷ η-at (K₀ X ⊗ I)
        ℂ.▷ K₁ (J₁ (ℂ.id (K₀ X) ⊗₁ (η-at I ℂ.▷ K₁ jd))
                𝕂.▷ (ε-at X ∥ ε-at I))
      ≡⟨ lemma1 ⟩
        η-at (K₀ X)
        ℂ.▷ K₁ (J₁ (ℂ.ρ-at (K₀ X))
          𝕂.▷ J₁ (ℂ.MonoidalProduct.F₁ (ℂ.id (K₀ X) , η-at (ℂ.Identity₀ tt)
            ℂ.▷ K₁ (𝕂.LikeI.F₁ tt)))
                  𝕂.▷ 𝕂.MonoidalLikeProduct.F₁ (ε-at X , ε-at (ℂ.Identity₀ tt)))
      ≡⟨ cong (λ x → (J₁ (ℂ.ρ-at (K₀ X)) 𝕂.▷ x ) ♯) ℍ.ich4a ⟩
        η-at (K₀ X)
        ℂ.▷ K₁ (J₁ (ℂ.ρ-at (K₀ X))
          𝕂.▷ (J₁ (ℂ.id (K₀ X)) 𝕂.▷ ε-at X) ∥ (J₁ (η-at I ℂ.▷ K₁ jd) 𝕂.▷ ε-at I))
      ≡⟨ cong (λ x → (J₁ (ℂ.ρ-at (K₀ X)) 𝕂.▷ (x 𝕂.▷ _) ∥ (J₁ (η-at I ℂ.▷ K₁ jd) 𝕂.▷ ε-at I))♯) J.strictIdentity ⟩
        η-at (K₀ X) ℂ.▷ K₁ (J₁ (ℂ.ρ-at (K₀ X)) 𝕂.▷ 𝕂.MonoidalLikeProduct.F₁ (𝕂.id (K₀ X) 𝕂.▷ ε-at X , J₁ (η-at (ℂ.Identity₀ tt) ℂ.▷ K₁ (𝕂.LikeI.F₁ tt)) 𝕂.▷ ε-at (ℂ.Identity₀ tt)))
      ≡⟨ cong (λ x → (J₁ (ℂ.ρ-at (K₀ X)) 𝕂.▷ x ∥ (J₁ (η-at I ℂ.▷ K₁ jd) 𝕂.▷ ε-at I))♯) 𝕂.▷lunit ⟩
        η-at (K₀ X) ℂ.▷ K₁ (J₁ (ℂ.ρ-at (K₀ X)) 𝕂.▷ 𝕂.MonoidalLikeProduct.F₁ (ε-at X , J₁ (η-at (ℂ.Identity₀ tt) ℂ.▷ K₁ (𝕂.LikeI.F₁ tt)) 𝕂.▷ ε-at (ℂ.Identity₀ tt)))
      ≡⟨ cong (λ x → (J₁ (ℂ.ρ-at (K₀ X)) 𝕂.▷ _ ∥ x)♯) ♯♭-bijection ⟩
        η-at (K₀ X) ℂ.▷ K₁ (J₁ (ℂ.ρ-at (K₀ X)) 𝕂.▷ ε-at X ∥ jd)
      ≡⟨ cong (λ x → (x 𝕂.▷ _)♯) refl ⟩
        η-at (K₀ X) ℂ.▷ K₁ (J₁ (ℂ.ρ-at (K₀ X)) 𝕂.▷ ε-at X ∥ jd)
      ≡⟨ cong (λ x → x ♯) ℍ.ρ-naturality ⟩
        η-at (K₀ X) ℂ.▷ K₁ (ε-at X 𝕂.▷ J₁ (ℂ.ρ-at X))
      ≡⟨ cong (λ x → (_ 𝕂.▷ x)♯) refl ⟩
        (η-at (K₀ X) ℂ.▷ K₁ (ε-at X 𝕂.▷ J₁ (ℂ.ρ-at X)))
      ≡⟨ lemma2 ⟩
        (η-at (K₀ X) ℂ.▷ K₁ (ε-at X)) ℂ.▷ K₁ (J₁ (ℂ.ρ-at X))
      ≡⟨ cong (λ x → x ℂ.▷ _) (sym zigzag-R) ⟩
        ℂ.id (K₀ X) ℂ.▷ K₁ (J₁ (ℂ.ρ-at X))
      ≡⟨ ℂ.▷lunit ⟩
        K₁ (J₁ (ℂ.ρ-at X))
      ∎
    ; diagram6 = λ {X Y Z} →
      begin
        ℂ.α-at (K₀ X) (K₀ Y) (K₀ Z)
        ℂ.▷ ℂ.id (K₀ X) ⊗₁ (η-at ((K₀ Y ⊗ K₀ Z))
          ℂ.▷ K₁ (ε-at Y ∥ ε-at Z))
        ℂ.▷ η-at (K₀ X ⊗ K₀ (Y ⊗ Z))
        ℂ.▷ K₁ (ε-at X ∥ ε-at (Y ⊗ Z))
      ≡⟨ cong (λ x → ℂ.α-at _ _ _ ℂ.▷ x) lemma1 ⟩
        ℂ.α-at (K₀ X) (K₀ Y) (K₀ Z)
        ℂ.▷ η-at (K₀ X ⊗ K₀ Y ⊗ K₀ Z)
        ℂ.▷ K₁ (J₁ (ℂ.id (K₀ X) ⊗₁ (η-at (K₀ Y ⊗ K₀ Z)
          ℂ.▷ K₁ (ε-at Y ∥ ε-at Z))) 𝕂.▷ (ε-at X ∥ ε-at (Y ⊗ Z)))
      ≡⟨ lemma1 ⟩
        η-at ((K₀ X ⊗ K₀ Y) ⊗ K₀ Z)
        ℂ.▷ K₁ (J₁ (ℂ.α-at (K₀ X) (K₀ Y) (K₀ Z))
          𝕂.▷ J₁ (ℂ.id (K₀ X) ⊗₁ (η-at (K₀ Y ⊗ K₀ Z) ℂ.▷ K₁ (ε-at Y ∥ ε-at Z))) 𝕂.▷ (ε-at X ∥ ε-at (Y ⊗ Z)))
      ≡⟨ cong (λ x → (J₁ (ℂ.α-at _ _ _) 𝕂.▷ x) ♯) ℍ.ich4a ⟩
        η-at ((K₀ X ⊗ K₀ Y) ⊗ K₀ Z)
        ℂ.▷ K₁ (J₁ (ℂ.α-at (K₀ X) (K₀ Y) (K₀ Z))
          𝕂.▷ (J₁ (ℂ.id (K₀ X)) 𝕂.▷ ε-at X) ∥ (J₁ (η-at (K₀ Y ⊗ K₀ Z) ℂ.▷ K₁ (ε-at Y ∥ ε-at Z)) 𝕂.▷ ε-at (Y ⊗ Z)))
      ≡⟨ cong (λ x → (J₁ (ℂ.α-at _ _ _) 𝕂.▷ (x 𝕂.▷ _) ∥  (J₁ (η-at (K₀ Y ⊗ K₀ Z) ℂ.▷ K₁ (ε-at Y ∥ ε-at Z)) 𝕂.▷ ε-at (Y ⊗ Z))) ♯) J.strictIdentity ⟩
        η-at ((K₀ X ⊗ K₀ Y) ⊗ K₀ Z)
        ℂ.▷ K₁ (J₁ (ℂ.α-at (K₀ X) (K₀ Y) (K₀ Z))
          𝕂.▷ (𝕂.id (K₀ X) 𝕂.▷ ε-at X) ∥ (J₁ (η-at (K₀ Y ⊗ K₀ Z) ℂ.▷ K₁ (ε-at Y ∥ ε-at Z)) 𝕂.▷ ε-at (Y ⊗ Z)))
      ≡⟨ cong (λ x → (J₁ (ℂ.α-at _ _ _) 𝕂.▷ x ∥  (J₁ (η-at (K₀ Y ⊗ K₀ Z) ℂ.▷ K₁ (ε-at Y ∥ ε-at Z)) 𝕂.▷ ε-at (Y ⊗ Z))) ♯) 𝕂.▷lunit ⟩
        (η-at ((K₀ X ⊗ K₀ Y) ⊗ K₀ Z)
        ℂ.▷ K₁ (J₁ (ℂ.α-at (K₀ X) (K₀ Y) (K₀ Z))
          𝕂.▷ ε-at X ∥ (J₁ (η-at (K₀ Y ⊗ K₀ Z) ℂ.▷ K₁ (ε-at Y ∥ ε-at Z)) 𝕂.▷ ε-at (Y ⊗ Z))))
      ≡⟨ cong (λ x → η-at ((K₀ X ⊗ K₀ Y) ⊗ K₀ Z)
        ℂ.▷ K₁ (J₁ (ℂ.α-at (K₀ X) (K₀ Y) (K₀ Z)) 𝕂.▷ ε-at X ∥ x)) ♯♭-bijection ⟩
          η-at ((K₀ X ⊗ K₀ Y) ⊗ K₀ Z) ℂ.▷ K₁ (J₁ (ℂ.α-at (K₀ X) (K₀ Y) (K₀ Z)) 𝕂.▷ ε-at X ∥ ε-at Y ∥ ε-at Z)
      ≡⟨ cong (λ x → ((x 𝕂.▷ _)♯)) refl ⟩
        η-at ((K₀ X ⊗ K₀ Y) ⊗ K₀ Z) ℂ.▷ K₁ (J₁ (ℂ.α-at (K₀ X) (K₀ Y) (K₀ Z)) 𝕂.▷ ε-at X ∥ ε-at Y ∥ ε-at Z)
      ≡⟨ cong (λ x → x ♯) (sym ℍ.α-naturality) ⟩
         ((ε-at X ∥ ε-at Y) ∥ ε-at Z 𝕂.▷ J₁ (ℂ.α-at X Y Z)) ♯
      ≡⟨ cong (λ x → (x ∥ ε-at Z 𝕂.▷ _)♯ ) (sym ♯♭-bijection) ⟩
        η-at ((K₀ X ⊗ K₀ Y) ⊗ K₀ Z) ℂ.▷
         K₁ ((J₁ (η-at (K₀ X ⊗ K₀ Y) ℂ.▷ K₁ (ε-at X ∥ ε-at Y)) 𝕂.▷ ε-at (X ⊗ Y)) ∥ ε-at Z
        𝕂.▷ J₁ (ℂ.α-at X Y Z))
      ≡⟨ cong (λ x → (((ε-at X ∥ ε-at Y)♯)♭ ∥ x 𝕂.▷ _)♯) (sym 𝕂.▷lunit) ⟩
        ((J₁ ((ε-at X ∥ ε-at Y)♯) 𝕂.▷ ε-at (X ⊗ Y)) ∥ (𝕂.id (K₀ Z) 𝕂.▷ ε-at Z) 𝕂.▷ J₁ (ℂ.α-at X Y Z))♯
      ≡⟨  cong (λ x → (((ε-at X ∥ ε-at Y)♯)♭ ∥ (x 𝕂.▷ _) 𝕂.▷ _)♯) (sym J.strictIdentity) ⟩
        ((J₁ ((ε-at X ∥ ε-at Y)♯) 𝕂.▷ ε-at (X ⊗ Y)) ∥ (J₁ (ℂ.id (K₀ Z)) 𝕂.▷ ε-at Z) 𝕂.▷ J₁ (ℂ.α-at X Y Z))♯ 
      ≡⟨ cong (λ x → (x 𝕂.▷ _)♯) (sym ℍ.ich4a) ⟩
        ((J₁ ((ε-at X ∥ ε-at Y)♯ ⊗₁ ℂ.id (K₀ Z)) 𝕂.▷ ε-at (X ⊗ Y) ∥ (ε-at Z)) 𝕂.▷ J₁ (ℂ.α-at X Y Z))♯
      ≡⟨ cong (λ x → x ♯) 𝕂.▷assoc ⟩
        ((J₁ ((ε-at X ∥ ε-at Y)♯ ⊗₁ ℂ.id (K₀ Z)) 𝕂.▷ ε-at (X ⊗ Y) ∥ (ε-at Z) 𝕂.▷ J₁ (ℂ.α-at X Y Z))♯)
      ≡⟨ sym lemma1 ⟩
        (ε-at X ∥ ε-at Y)♯ ⊗₁ ℂ.id (K₀ Z) ℂ.▷ (ε-at (X ⊗ Y) ∥ (ε-at Z) 𝕂.▷ J₁ (ℂ.α-at X Y Z))♯
      ≡⟨ cong (λ x → (ε-at X ∥ ε-at Y)♯ ⊗₁ ℂ.id (K₀ Z) ℂ.▷ (ε-at (X ⊗ Y) ∥ (ε-at Z) 𝕂.▷ x)♯) refl ⟩
        ((ε-at X ∥ ε-at Y)♯ ⊗₁ ℂ.id (K₀ Z) ℂ.▷ (ε-at (X ⊗ Y) ∥ (ε-at Z) 𝕂.▷ J₁ (ℂ.α-at X Y Z))♯)
      ≡⟨ cong (λ x → ((ε-at X ∥ ε-at Y)♯ ⊗₁ ℂ.id (K₀ Z) ℂ.▷ x)) lemma2 ⟩
        (ε-at X ∥ ε-at Y)♯ ⊗₁ ℂ.id (K₀ Z) ℂ.▷ ((ε-at ((X ⊗ Y)) ∥ ε-at Z)♯) ℂ.▷ K₁ (J₁ (ℂ.α-at X Y Z))
      ∎
    ; inequation1 = let open ≤-Reasoning {ℂ} in
      ≤begin
        η-at I
      ≦⟨ ℂ.▷runit ⟩
        η-at I ℂ.▷ ℂ.id (K₀ I)
      ≦⟨ cong (λ x → η-at I ℂ.▷ x) (sym K.strictIdentity) ⟩
        η-at I ℂ.▷ K₁ (𝕂.id I)
      ≤⟨ ℂ.▷monot≤ ℂ.≤refl (K.preserveOrder 𝕂.LikeI.laxIdentity) ⟩
        η-at I ℂ.▷ K₁ jd
      ≤∎
    -- make this proof only use ♯ and ♭
    ; inequation2 = let open ≤-Reasoning {ℂ} in
      ≤begin
        (η-at I ℂ.▷ K₁ jd) ℂ.▷ K₁ (J₁ (η-at I ℂ.▷ K₁ jd)) ℂ.▷ K₁ (ε-at I)
      ≦⟨ cong (λ x → (η-at I ℂ.▷ K₁ jd) ℂ.▷ x) (sym K.strictComposition) ⟩
        (η-at I ℂ.▷ K₁ jd) ℂ.▷ K₁ (J₁ (η-at I ℂ.▷ K₁ jd) 𝕂.▷ ε-at I)
      ≦⟨ ℂ.▷assoc ⟩
        η-at I ℂ.▷ K₁ jd ℂ.▷ K₁ (J₁ (η-at I ℂ.▷ K₁ jd) 𝕂.▷ ε-at I)
      ≦⟨ cong (λ x → η-at I ℂ.▷ x) (sym K.strictComposition)⟩
        (jd 𝕂.▷ (jd ♯)♭)♯
      ≦⟨ cong (λ x → (jd 𝕂.▷ x)♯) ♯♭-bijection ⟩
        (jd 𝕂.▷ jd)♯
      ≤⟨ ℂ.▷monot≤ ℂ.≤refl (K.preserveOrder 𝕂.LikeI.laxComposition) ⟩
        jd ♯
      ≤∎
    ; inequation3 = λ {X Y} → let open ≤-Reasoning {ℂ} in
      ≤begin
        η-at (X ⊗ Y)
      ≦⟨ ℂ.▷runit ⟩
        η-at (X ⊗ Y) ℂ.▷ ℂ.id (K₀ (X ⊗ Y))
      ≦⟨ cong (λ x → η-at _ ℂ.▷ x) (sym K.strictIdentity) ⟩
        𝕂.id ((X ⊗ Y)) ♯
      ≤⟨ ℂ.▷monot≤ ℂ.≤refl
          (K.preserveOrder 𝕂.MonoidalLikeProduct.laxIdentity) ⟩
        (𝕂.id  X ∥ 𝕂.id Y) ♯
      ≦⟨ psi-lemma ⟩
        𝕂.id X ♯ ⊗₁ 𝕂.id Y ♯ ℂ.▷ (ε-at X ∥ ε-at Y) ♯
      ≦⟨ cong (λ x → (η-at X ℂ.▷ x) ⊗₁ 𝕂.id Y ♯ ℂ.▷ (ε-at X ∥ ε-at Y) ♯) K.strictIdentity ⟩
        ((η-at X ℂ.▷ ℂ.id (K₀ X)) ⊗₁ 𝕂.id Y ♯ ℂ.▷ (ε-at X ∥ ε-at Y) ♯)
      ≦⟨ cong (λ x → x ⊗₁ 𝕂.id Y ♯ ℂ.▷ (ε-at X ∥ ε-at Y) ♯) (sym ℂ.▷runit) ⟩
        η-at X ⊗₁ (η-at Y ℂ.▷ K₁ (𝕂.id Y)) ℂ.▷
         η-at (K₀ X ⊗ K₀ Y) ℂ.▷ K₁ (ε-at X ∥ ε-at Y)
      ≦⟨ cong (λ x → _ ⊗₁ (η-at Y ℂ.▷ x) ℂ.▷ (ε-at X ∥ ε-at Y) ♯) K.strictIdentity ⟩
        η-at X ⊗₁ (η-at Y ℂ.▷ ℂ.id (K₀ Y)) ℂ.▷
         η-at (K₀ X ⊗ K₀ Y) ℂ.▷ K₁ (ε-at X ∥ ε-at Y)
      ≦⟨ cong (λ x → _ ⊗₁ x ℂ.▷ (ε-at X ∥ ε-at Y) ♯) (sym ℂ.▷runit) ⟩
        η-at X ⊗₁ η-at Y ℂ.▷ (ε-at X ∥ ε-at Y)♯
      ≤∎
    ; inequation4 = λ {X Y} → let open ≤-Reasoning {ℂ} in
      ≤begin
        (η-at (K₀ (K₀ X) ⊗ K₀ (K₀ Y)) ℂ.▷ K₁ (ε-at (K₀ X) ∥ ε-at (K₀ Y))) ℂ.▷
         K₁ (J₁ (η-at (K₀ X ⊗ K₀ Y) ℂ.▷ K₁ (ε-at X ∥ ε-at Y)))
         ℂ.▷ K₁ (ε-at (X ⊗ Y))
      ≦⟨ sym mi-lemma ⟩
        (ε-at (K₀ X) ∥ ε-at (K₀ Y) 𝕂.▷ ε-at X ∥ ε-at Y) ♯
      ≤⟨ ℂ.▷monot≤ ℂ.≤refl (K.preserveOrder 𝕂.MonoidalLikeProduct.laxComposition) ⟩
         ((ε-at (K₀ X) 𝕂.▷ ε-at X) ∥ (ε-at (K₀ Y) 𝕂.▷ ε-at Y)) ♯
      ≦⟨ cong (λ x → (x ∥ (ε-at (K₀ Y) 𝕂.▷ ε-at Y))♯) (sym ε-naturality) ⟩
        ((J₁ (K₁ (ε-at X)) 𝕂.▷ ε-at X) ∥ (ε-at (K₀ Y) 𝕂.▷ ε-at Y)) ♯
      ≦⟨ cong (λ x → ((J₁ (K₁ (ε-at X)) 𝕂.▷ ε-at X) ∥ x) ♯) (sym ε-naturality) ⟩
        ((J₁ (K₁ (ε-at X)) 𝕂.▷ ε-at X) ∥ (J₁ (K₁ (ε-at Y)) 𝕂.▷ ε-at Y)) ♯
      ≦⟨ cong _♯ (sym ℍ.ich4a) ⟩
        (J₁ (K₁ (ε-at X) ⊗₁ K₁ (ε-at Y)) 𝕂.▷ (ε-at X) ∥ (ε-at Y)) ♯
      ≦⟨ sym lemma1 ⟩
        K₁ (ε-at X) ⊗₁ K₁ (ε-at Y) ℂ.▷ η-at (K₀ X ⊗ K₀ Y) ℂ.▷ K₁ (ε-at X ∥ ε-at Y)
      ≤∎
    }