{-# OPTIONS --without-K --safe #-}

open import Categories.Bicategory
open import Categories.Bicategory.Monad using (Monad)

module Categories.Bicategory.Monad.Bimodule.Homomorphism {o  e t} {𝒞 : Bicategory o  e t} {M₁ M₂ : Monad 𝒞} where

open import Level
open import Categories.Bicategory.Monad.Bimodule using (Bimodule)
import Categories.Bicategory.Extras as Bicat
open Bicat 𝒞
import Categories.Morphism.Reasoning as MR

private
  module MR' {A B : Obj} where
    open MR (hom A B) public

record Bimodulehomomorphism (B₁ B₂ : Bimodule M₁ M₂) : Set (  e) where
  open Monad using (T)
  open Bimodule using (F; actionˡ; actionʳ)
  field
    α       : F B₁ ⇒₂ F B₂
    linearˡ : actionˡ B₂ ∘ᵥ (α  T M₁)  α ∘ᵥ actionˡ B₁
    linearʳ : actionʳ B₂ ∘ᵥ (T M₂  α)  α ∘ᵥ actionʳ B₁

id-bimodule-hom : {B : Bimodule M₁ M₂}  Bimodulehomomorphism B B
id-bimodule-hom {B} = record
  { α = id₂
  ; linearˡ = id-linearˡ
  ; linearʳ = id-linearʳ
  }
  where
    open Monad using (C; T)
    open Bimodule B using (actionˡ; actionʳ)
    open hom.HomReasoning
    open MR'

    id-linearˡ : actionˡ ∘ᵥ (id₂  T M₁)  id₂ ∘ᵥ actionˡ
    id-linearˡ = begin
      actionˡ ∘ᵥ (id₂  T M₁) ≈⟨ elimʳ ▷id₂ 
      actionˡ                 ≈⟨  identity₂ˡ 
      id₂ ∘ᵥ actionˡ          

    id-linearʳ : actionʳ ∘ᵥ (T M₂  id₂)  id₂ ∘ᵥ actionʳ
    id-linearʳ = begin
      actionʳ ∘ᵥ (T M₂  id₂) ≈⟨ elimʳ ▷id₂ 
      actionʳ                 ≈⟨  identity₂ˡ 
      id₂ ∘ᵥ actionʳ          

bimodule-hom-∘ : {B₁ B₂ B₃ : Bimodule M₁ M₂}
                Bimodulehomomorphism B₂ B₃  Bimodulehomomorphism B₁ B₂  Bimodulehomomorphism B₁ B₃
bimodule-hom-∘ {B₁} {B₂} {B₃} g f = record
  { α = α g ∘ᵥ α f
  ; linearˡ = g∘f-linearˡ
  ; linearʳ = g∘f-linearʳ
  }
  where
    open Monad using (C; T)
    open Bimodule using (F; actionˡ; actionʳ)
    open Bimodulehomomorphism using (α; linearˡ; linearʳ)
    open hom.HomReasoning
    open MR'

    g∘f-linearˡ : actionˡ B₃ ∘ᵥ (α g ∘ᵥ α f)  T M₁  (α g ∘ᵥ α f) ∘ᵥ actionˡ B₁
    g∘f-linearˡ = begin
      actionˡ B₃ ∘ᵥ (α g ∘ᵥ α f)  T M₁            ≈⟨ refl⟩∘⟨  ∘ᵥ-distr-◁ 
      actionˡ B₃ ∘ᵥ (α g  T M₁) ∘ᵥ (α f  T M₁)   ≈⟨ glue′ (linearˡ g) (linearˡ f) 
      (α g ∘ᵥ α f) ∘ᵥ actionˡ B₁                   

    g∘f-linearʳ : actionʳ B₃ ∘ᵥ T M₂  (α g ∘ᵥ α f)  (α g ∘ᵥ α f) ∘ᵥ actionʳ B₁
    g∘f-linearʳ = begin
      actionʳ B₃ ∘ᵥ T M₂  (α g ∘ᵥ α f)            ≈⟨ refl⟩∘⟨ ( ∘ᵥ-distr-▷) 
      actionʳ B₃ ∘ᵥ (T M₂  α g) ∘ᵥ (T M₂  α f)   ≈⟨ glue′ (linearʳ g) (linearʳ f) 
      (α g ∘ᵥ α f) ∘ᵥ actionʳ B₁