Merge pull request #481 from tillrampe/cat-of-bimods

Properties of the 1-Category of Bimodules

Author: JacquesCarette

src/Categories/Category/Construction/Bimodules/Properties.agda

@@ -7,35 +7,32 @@ open import Categories.Bicategory.Monad
 module Categories.Category.Construction.Bimodules.Properties
   {o ℓ e t} {𝒞 : Bicategory o ℓ e t} {M₁ M₂ : Monad 𝒞} where
 
-open import Agda.Primitive
-
-import Categories.Category.Construction.Bimodules
-open import Categories.Category
-
-Bimodules : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e
-Bimodules = Categories.Category.Construction.Bimodules.Bimodules M₁ M₂
+open import Categories.Bicategory.Monad.Bimodule using (Bimodule)
+open import Categories.Bicategory.Monad.Bimodule.Homomorphism using (Bimodulehomomorphism)
+import Categories.Morphism as Mor
+import Categories.Morphism.Reasoning.Iso as IsoReasoning
+open import Categories.Category.Construction.Bimodules M₁ M₂ using (Bimodules)
+open import Categories.Category using (Category)
+import Categories.Bicategory.Extras as Bicat
 
 private
-  module Cat {o₁ ℓ₁ e₁} {C : Categories.Category.Category o₁ ℓ₁ e₁} where
-    open Categories.Category.Category C using (Obj; _⇒_) public
-    open import Categories.Morphism C using (IsIso; _≅_) public
-    open import Categories.Morphism.Reasoning.Iso C using (conjugate-from) public
+  module Bimodules where
+    open Category Bimodules public
+    open Mor Bimodules using (IsIso; _≅_) public
 
-open Cat
-
-
-import Categories.Bicategory.Extras as Bicat
-open Bicat 𝒞 using (hom; _⇒₂_; _≈_; _∘ᵥ_; _◁_; _▷_; _◁ᵢ_; _▷ᵢ_)
+  module 𝒞 where
+    open Bicat 𝒞 public
 
-open import Categories.Bicategory.Monad.Bimodule {𝒞 = 𝒞}
-open import Categories.Bicategory.Monad.Bimodule.Homomorphism {𝒞 = 𝒞}
+  module HomCat {A B : 𝒞.Obj} where
+    open Mor (𝒞.hom A B) using (IsIso; _≅_) public
+    open IsoReasoning (𝒞.hom A B) using (conjugate-from) public
 
-module Bimodulehom-isIso {B₁ B₂ : Obj {C = Bimodules}} (f : _⇒_ {C = Bimodules} B₁ B₂) where
+module Bimodule-Isomorphism {B₁ B₂ : Bimodules.Obj} (f : B₁ Bimodules.⇒ B₂) where
   open Monad using (C; T)
   open Bimodule using (F; actionˡ; actionʳ)
   open Bimodulehomomorphism f using (α; linearˡ; linearʳ)
 
-  αisIso⇒fisIso : IsIso {C = hom (C M₁) (C M₂)} α → IsIso {C = Bimodules} f
+  αisIso⇒fisIso : HomCat.IsIso α → Bimodules.IsIso f
   αisIso⇒fisIso αisIso = record
     { inv = record
       { α = α⁻¹
@@ -44,32 +41,32 @@ module Bimodulehom-isIso {B₁ B₂ : Obj {C = Bimodules}} (f : _⇒_ {C = Bimod
       }
     ; iso = record
     -- Cannot be delta reduced because of size issues
-      { isoˡ = IsIso.isoˡ αisIso
-      ; isoʳ = IsIso.isoʳ αisIso
+      { isoˡ = HomCat.IsIso.isoˡ αisIso
+      ; isoʳ = HomCat.IsIso.isoʳ αisIso
       }
     }
     where
-      open hom.HomReasoning
+      open 𝒞.hom.HomReasoning
 
-      α⁻¹ : F B₂ ⇒₂ F B₁
-      α⁻¹ = IsIso.inv αisIso
+      α⁻¹ : F B₂ 𝒞.⇒₂ F B₁
+      α⁻¹ = HomCat.IsIso.inv αisIso
 
-      αIso : F B₁ ≅ F B₂
+      αIso : F B₁ HomCat.≅ F B₂
       αIso = record
         { from = α
         ; to = α⁻¹
-        ; iso = IsIso.iso αisIso
+        ; iso = HomCat.IsIso.iso αisIso
         }
 
-      linearˡ⁻¹ : actionˡ B₁ ∘ᵥ α⁻¹ ◁ T M₁ ≈ α⁻¹ ∘ᵥ actionˡ B₂
-      linearˡ⁻¹ = ⟺ (conjugate-from (αIso ◁ᵢ T M₁) αIso linearˡ)
+      linearˡ⁻¹ : actionˡ B₁ 𝒞.∘ᵥ α⁻¹ 𝒞.◁ T M₁ 𝒞.≈ α⁻¹ 𝒞.∘ᵥ actionˡ B₂
+      linearˡ⁻¹ = ⟺ (HomCat.conjugate-from (αIso 𝒞.◁ᵢ T M₁) αIso linearˡ)
 
-      linearʳ⁻¹ : actionʳ B₁ ∘ᵥ T M₂ ▷ α⁻¹ ≈ α⁻¹ ∘ᵥ actionʳ B₂
-      linearʳ⁻¹ = ⟺ (conjugate-from (T M₂ ▷ᵢ αIso) αIso linearʳ)
+      linearʳ⁻¹ : actionʳ B₁ 𝒞.∘ᵥ T M₂ 𝒞.▷ α⁻¹ 𝒞.≈ α⁻¹ 𝒞.∘ᵥ actionʳ B₂
+      linearʳ⁻¹ = ⟺ (HomCat.conjugate-from (T M₂ 𝒞.▷ᵢ αIso) αIso linearʳ)
 
-  αisIso⇒Iso : IsIso {C = hom (C M₁) (C M₂)} α → B₁ ≅ B₂
+  αisIso⇒Iso : HomCat.IsIso α → B₁ Bimodules.≅ B₂
   αisIso⇒Iso αisIso = record
     { from = f
-    ; to = IsIso.inv (αisIso⇒fisIso αisIso)
-    ; iso = IsIso.iso (αisIso⇒fisIso αisIso)
+    ; to = Bimodules.IsIso.inv (αisIso⇒fisIso αisIso)
+    ; iso = Bimodules.IsIso.iso (αisIso⇒fisIso αisIso)
     }