{-# OPTIONS --without-K --safe --lossy-unification #-}
-- lossy unification is required to complete type-checking

open import Categories.Bicategory
open import Categories.Bicategory.LocalCoequalizers

module Categories.Bicategory.Construction.Bimodules {o ℓ e t} (𝒞 : Bicategory o ℓ e t) (localCoeq : LocalCoequalizers 𝒞) where
open import Level using (_⊔_)
open import Data.Product using (_,_)

import Categories.Bicategory.Extras as Bicat
open Bicat 𝒞

open import Categories.Bicategory.Monad using (Monad)
open import Categories.Bicategory.Monad.Bimodule using (Bimodule; id-bimodule)

open import Categories.Category.Construction.Bimodules {𝒞 = 𝒞} using ()renaming (Bimodules to 1-Bimodules)
open import Categories.Category using (Category)
private
  module 1-Bimodules M₁ M₂ = Category (1-Bimodules M₁ M₂)

open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
open import Categories.Morphism using (_≅_)

open import Categories.Bicategory.Construction.Bimodules.TensorproductOfBimodules localCoeq using () renaming (Tensorproduct to infixr  _⊗₀_)
open import Categories.Bicategory.Construction.Bimodules.TensorproductOfHomomorphisms localCoeq using () renaming (Tensorproduct to infixr  _⊗₁_)
open import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Functorial localCoeq
open import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Associator localCoeq using (associator-⊗)
open import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Associator.Naturality localCoeq using (α⇒-⊗-natural)
open import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Unitor localCoeq using (module Left-Unitor; module Right-Unitor)
open Left-Unitor using (unitorˡ-⊗)
open Right-Unitor using (unitorʳ-⊗)
open import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Unitor.Naturality localCoeq
  using (module Left-Unitor-natural; module Right-Unitor-natural)
open Left-Unitor-natural using (λ⇒-⊗-natural)
open Right-Unitor-natural using (ρ⇒-⊗-natural)
open import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Coherence.Pentagon localCoeq using (pentagon-⊗)
open import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Coherence.Triangle localCoeq using (triangle-⊗)

Bimodules : Bicategory (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e (o ⊔ ℓ ⊔ e ⊔ t)
Bimodules = record
  { enriched = record
    { Obj = Monad 𝒞
    ; hom = 1-Bimodules
    ; id = λ {M} → record
    { F₀ = λ _ → id-bimodule M
    ; F₁ = λ _ → 1-Bimodules.id M M
    ; identity = hom.Equiv.refl
    ; homomorphism = hom.Equiv.sym (1-Bimodules.identity² M M)
    ; F-resp-≈ = λ _ → hom.Equiv.refl
    }
    ; ⊚ = record
      { F₀ = λ (B₂ , B₁) → B₂ ⊗₀ B₁
      ; F₁ = λ (h₂ , h₁) → h₂ ⊗₁ h₁
      ; identity = λ {(B₂ , B₁)} → Identity.⊗₁-resp-id₂ B₂ B₁
      ; homomorphism = λ {_} {_} {_} {(g₂ , g₁)} {(h₂ , h₁)} → Composition.⊗₁-distr-∘ᵥ h₂ h₁ g₂ g₁
      ; F-resp-≈ = λ {_} {_} {(h₂ , h₁)} {(h'₂ , h'₁)} (e₂ , e₁) → ≈Preservation.⊗₁-resp-≈ h₂ h'₂ h₁ h'₁ e₂ e₁
      }
    ; ⊚-assoc = niHelper record
      { η = λ ((B₃ , B₂) , B₁) → _≅_.from (associator-⊗ {B₃ = B₃} {B₂} {B₁})
      ; η⁻¹ = λ ((B₃ , B₂) , B₁) → _≅_.to (associator-⊗ {B₃ = B₃} {B₂} {B₁})
      ; commute = λ ((f₃ , f₂) , f₁) → α⇒-⊗-natural f₃ f₂ f₁
      ; iso = λ ((B₃ , B₂) , B₁) → _≅_.iso (associator-⊗ {B₃ = B₃} {B₂} {B₁})
      }
    ; unitˡ = niHelper record
      { η = λ (_ , B) → _≅_.from (unitorˡ-⊗ {B = B})
      ; η⁻¹ = λ (_ , B) → _≅_.to (unitorˡ-⊗ {B = B})
      ; commute = λ (_ , f) → λ⇒-⊗-natural f
      ; iso = λ (_ , B) → _≅_.iso (unitorˡ-⊗ {B = B})
      }
    ; unitʳ = niHelper record
      { η = λ (B , _) → _≅_.from (unitorʳ-⊗ {B = B})
      ; η⁻¹ = λ (B , _) → _≅_.to (unitorʳ-⊗ {B = B})
      ; commute = λ (f , _) → ρ⇒-⊗-natural f
      ; iso = λ (B , _) → _≅_.iso (unitorʳ-⊗ {B = B})
      }
    }
  ; triangle = λ {_} {_} {_} {B₁} {B₂} → triangle-⊗ {B₂ = B₂} {B₁}
  ; pentagon = λ {_} {_} {_} {_} {_} {B₁} {B₂} {B₃} {B₄} → pentagon-⊗ {B₄ = B₄} {B₃} {B₂} {B₁}
  }