{-# OPTIONS --without-K --safe #-}
open import Categories.Bicategory
open import Categories.Bicategory.Monad using (Monad)
module Categories.Category.Construction.Bimodules {o ℓ e t} {𝒞 : Bicategory o ℓ e t} (M₁ M₂ : Monad 𝒞) where
open import Level
open import Categories.Category
open import Categories.Bicategory.Monad.Bimodule using (Bimodule)
open import Categories.Bicategory.Monad.Bimodule.Homomorphism using (Bimodulehomomorphism; id-bimodule-hom; bimodule-hom-∘)
import Categories.Bicategory.Extras as Bicat
open Bicat 𝒞
Bimodules : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e
Bimodules = record
{ Obj = Bimodule M₁ M₂
; _⇒_ = Bimodulehomomorphism
; _≈_ = λ h₁ h₂ → α h₁ ≈ α h₂
; id = id-bimodule-hom
; _∘_ = bimodule-hom-∘
; assoc = assoc₂
; sym-assoc = sym-assoc₂
; identityˡ = identity₂ˡ
; identityʳ = identity₂ʳ
; identity² = identity₂²
; equiv = record
{ refl = hom.Equiv.refl
; sym = hom.Equiv.sym
; trans = hom.Equiv.trans
}
; ∘-resp-≈ = hom.∘-resp-≈
}
where
open Bimodulehomomorphism using (α)