Merge pull request #482 from tillrampe/bicat-of-bimods

Bicat of bimods

Author: JacquesCarette

src/Categories/Bicategory/Construction/Bimodules.agda

@@ -0,0 +1,80 @@
+{-# 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 30 _⊗₀_)
+open import Categories.Bicategory.Construction.Bimodules.TensorproductOfHomomorphisms localCoeq using () renaming (Tensorproduct to infixr 30 _⊗₁_)
+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₁}
+  }