Fixed formatting and made modules private as requested

Author: djlowther

src/Categories/Bicategory/Object/Product.agda

@@ -48,9 +48,10 @@ record Product (A B : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
     η₂ : ∀ {Γ}{p p'}(ϕ : hom Γ A×B [ p , p' ])
        → Along (η₁ _) , (η₁ _) [ ϕ ≈ ⟨ πa ▷ ϕ , πb ▷ ϕ ⟩₂ ]
 
-  module β₁a {Γ} f g = _≅_ (β₁a {Γ} f g)
-  module β₁b {Γ} f g = _≅_ (β₁b {Γ} f g)
-  module η₁ {Γ} p = _≅_ (η₁ {Γ} p)
+  private
+    module β₁a {Γ} f g = _≅_ (β₁a {Γ} f g)
+    module β₁b {Γ} f g = _≅_ (β₁b {Γ} f g)
+    module η₁ {Γ} p = _≅_ (η₁ {Γ} p)
 
   unique₂ : ∀ {Γ}{p p'}{ϕ ψ : hom Γ A×B [ p , p' ]} → πa ▷ ϕ ≈ πa ▷ ψ → πb ▷ ϕ ≈ πb ▷ ψ → ϕ ≈ ψ
   unique₂ {ϕ = ϕ}{ψ} ϕa≈ψa ϕb≈ψb = begin
@@ -63,23 +64,29 @@ record Product (A B : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
   ⟨-,-⟩ = record
     { F₀ = uncurry′ ⟨_,_⟩₁
     ; F₁ = uncurry′ ⟨_,_⟩₂
-    ; identity = unique₂ (MR′.switch-fromtoˡ (β₁a _ _) (β₂a id₂ id₂) ○ hom.∘-resp-≈ʳ identity₂ˡ
-                           ○ β₁a.isoˡ _ _ ○ ⟺ ⊚.identity)
-                         (MR′.switch-fromtoˡ (β₁b _ _) (β₂b id₂ id₂) ○ hom.∘-resp-≈ʳ identity₂ˡ
-                           ○ β₁b.isoˡ _ _ ○ ⟺ ⊚.identity)
-    ; homomorphism = λ{_ _ _ (αa , αb) (βa , βb)}
-                   → unique₂ (MR′.switch-fromtoˡ (β₁a _ _) (β₂a (βa ∘ᵥ αa) (βb ∘ᵥ αb))
-                                ○ MR′.pushʳ (MR′.extendˡ (MR′.insertˡ (β₁a.isoʳ _ _)))
-                                ○ ⟺ (MR′.switch-fromtoˡ (β₁a _ _) (β₂a βa βb)
-                                        ⟩∘⟨ MR′.switch-fromtoˡ (β₁a _ _) (β₂a αa αb))
-                                ○ ∘ᵥ-distr-▷)
-                             (MR′.switch-fromtoˡ (β₁b _ _) (β₂b (βa ∘ᵥ αa) (βb ∘ᵥ αb))
-                                ○ MR′.pushʳ (MR′.extendˡ (MR′.insertˡ (β₁b.isoʳ _ _)))
-                                ○ ⟺ (MR′.switch-fromtoˡ (β₁b _ _) (β₂b βa βb)
-                                        ⟩∘⟨ MR′.switch-fromtoˡ (β₁b _ _) (β₂b αa αb))
-                                ○ ∘ᵥ-distr-▷)
+    ; identity = ⟨⟩-identity
+    ; homomorphism = ⟨⟩-homomorphism
     ; F-resp-≈ = uncurry′ ⟨⟩-resp-≈
     }
+    where
+      ⟨⟩-identity : ∀ {Γ}{f : Γ ⇒₁ A}{g : Γ ⇒₁ B} → ⟨ id₂ {f = f} , id₂ {f = g} ⟩₂ ≈ id₂
+      ⟨⟩-identity = unique₂ (MR′.switch-fromtoˡ (β₁a _ _) (β₂a id₂ id₂) ○ hom.∘-resp-≈ʳ identity₂ˡ
+                              ○ β₁a.isoˡ _ _ ○ ⟺ ⊚.identity)
+                            (MR′.switch-fromtoˡ (β₁b _ _) (β₂b id₂ id₂) ○ hom.∘-resp-≈ʳ identity₂ˡ
+                              ○ β₁b.isoˡ _ _ ○ ⟺ ⊚.identity)
+      ⟨⟩-homomorphism : ∀ {Γ}{fa ga ha : Γ ⇒₁ A}{fb gb hb : Γ ⇒₁ B}
+                      → {αa : fa ⇒₂ ga}{αb : fb ⇒₂ gb}{βa : ga ⇒₂ ha}{βb : gb ⇒₂ hb}
+                      → ⟨ βa ∘ᵥ αa , βb ∘ᵥ αb ⟩₂ ≈ ⟨ βa , βb ⟩₂ ∘ᵥ ⟨ αa , αb ⟩₂
+      ⟨⟩-homomorphism {αa = αa}{αb}{βa}{βb} = unique₂ (MR′.switch-fromtoˡ (β₁a _ _) (β₂a (βa ∘ᵥ αa) (βb ∘ᵥ αb))
+                                                        ○ MR′.pushʳ (MR′.extendˡ (MR′.insertˡ (β₁a.isoʳ _ _)))
+                                                        ○ ⟺ (MR′.switch-fromtoˡ (β₁a _ _) (β₂a βa βb)
+                                                              ⟩∘⟨ MR′.switch-fromtoˡ (β₁a _ _) (β₂a αa αb))
+                                                        ○ ∘ᵥ-distr-▷)
+                                                      (MR′.switch-fromtoˡ (β₁b _ _) (β₂b (βa ∘ᵥ αa) (βb ∘ᵥ αb))
+                                                        ○ MR′.pushʳ (MR′.extendˡ (MR′.insertˡ (β₁b.isoʳ _ _)))
+                                                        ○ ⟺ (MR′.switch-fromtoˡ (β₁b _ _) (β₂b βa βb)
+                                                              ⟩∘⟨ MR′.switch-fromtoˡ (β₁b _ _) (β₂b αa αb))
+                                                        ○ ∘ᵥ-distr-▷)
 
   βa : ∀ {Γ} → πa ⊚- ∘F ⟨-,-⟩ {Γ} ≃ πˡ
   βa = pointwise-iso (uncurry β₁a) (uncurry β₂a)
@@ -94,5 +101,11 @@ record Product (A B : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
   η = pointwise-iso η₁ η₂
 
   𝒞[Γ,A×B]≅𝒞[Γ,A]×𝒞[Γ,B] : ∀ {Γ} → StrongEquivalence (hom Γ A×B) (CatProduct (hom Γ A) (hom Γ B))
-  𝒞[Γ,A×B]≅𝒞[Γ,A]×𝒞[Γ,B] = record { F = πa ⊚- ※ πb ⊚- ; G = ⟨-,-⟩
-                                  ; weak-inverse = record { F∘G≈id = β ; G∘F≈id = sym η } }
+  𝒞[Γ,A×B]≅𝒞[Γ,A]×𝒞[Γ,B] = record
+    { F = πa ⊚- ※ πb ⊚-
+    ; G = ⟨-,-⟩
+    ; weak-inverse = record
+      { F∘G≈id = β
+      ; G∘F≈id = sym η
+      }
+    }