Merge pull request #505 from djlowther/2-product-fix

Bicategory.Object.Product improvements

Author: JacquesCarette

src/Categories/Bicategory/Object/Product.agda

@@ -4,14 +4,28 @@ open import Categories.Bicategory using (Bicategory)
 module Categories.Bicategory.Object.Product {o ℓ e t} (𝒞 : Bicategory o ℓ e t) where
 
 open import Level
+open import Data.Product using (_,_; uncurry; uncurry′)
 
-open Bicategory 𝒞
+open import Categories.Bicategory.Extras 𝒞
 open import Categories.Category using (_[_,_])
+open import Categories.Category.Equivalence using (StrongEquivalence)
+open import Categories.Category.Product using (_※_; _※ⁿⁱ_; πˡ; πʳ) renaming (Product to CatProduct)
+open import Categories.Functor using (_∘F_) renaming (id to idF)
+open import Categories.Functor.Bifunctor using (Bifunctor)
 open import Categories.Morphism using (_≅_)
 open import Categories.Morphism.HeterogeneousEquality
 open import Categories.Morphism.Notation using (_[_≅_])
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; sym)
+open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (pointwise-iso)
 
-record Product  (A B : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
+import Categories.Morphism.Reasoning as MR
+
+open hom.HomReasoning
+
+private
+  module MR′ {X Y} = MR (hom X Y)
+
+record Product (A B : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
   infix 10 ⟨_,_⟩₁ ⟨_,_⟩₂
   field
     A×B : Obj
@@ -20,6 +34,8 @@ record Product  (A B : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
     ⟨_,_⟩₁ : ∀ {Γ} → Γ ⇒₁ A → Γ ⇒₁ B → Γ ⇒₁ A×B
     ⟨_,_⟩₂ : ∀ {Γ}{fa ga : Γ ⇒₁ A}{fb gb : Γ ⇒₁ B}
            → fa ⇒₂ ga → fb ⇒₂ gb → ⟨ fa , fb ⟩₁ ⇒₂ ⟨ ga , gb ⟩₁
+    ⟨⟩-resp-≈ : ∀ {Γ}{fa ga : Γ ⇒₁ A}{fb gb : Γ ⇒₁ B}{αa βa : fa ⇒₂ ga}{αb βb : fb ⇒₂ gb}
+              → αa ≈ βa → αb ≈ βb → ⟨ αa , αb ⟩₂ ≈ ⟨ βa , βb ⟩₂
 
     β₁a : ∀ {Γ} f g → hom Γ A [ πa ∘₁ ⟨ f , g ⟩₁  ≅ f ]
     β₁b : ∀ {Γ} f g → hom Γ B [ πb ∘₁ ⟨ f , g ⟩₁  ≅ g ]
@@ -31,3 +47,65 @@ record Product  (A B : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
     η₁ : ∀ {Γ} p → hom Γ A×B [ p ≅ ⟨ πa ∘₁ p , πb ∘₁ p ⟩₁ ]
     η₂ : ∀ {Γ}{p p'}(ϕ : hom Γ A×B [ p , p' ])
        → Along (η₁ _) , (η₁ _) [ ϕ ≈ ⟨ πa ▷ ϕ , πb ▷ ϕ ⟩₂ ]
+
+  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
+    ϕ                                             ≈⟨ MR′.switch-fromtoˡ (η₁ _) (η₂ ϕ) ⟩
+    η₁.to _ ∘ᵥ ⟨ πa ▷ ϕ , πb ▷ ϕ ⟩₂ ∘ᵥ η₁.from _  ≈⟨ refl⟩∘⟨ ⟨⟩-resp-≈ ϕa≈ψa ϕb≈ψb ⟩∘⟨refl ⟩
+    η₁.to _ ∘ᵥ ⟨ πa ▷ ψ , πb ▷ ψ ⟩₂ ∘ᵥ η₁.from _  ≈⟨ ⟺ (MR′.switch-fromtoˡ (η₁ _) (η₂ ψ)) ⟩
+    ψ                                             ∎
+
+  ⟨-,-⟩ : ∀ {Γ} → Bifunctor (hom Γ A) (hom Γ B) (hom Γ A×B)
+  ⟨-,-⟩ = record
+    { F₀ = uncurry′ ⟨_,_⟩₁
+    ; F₁ = uncurry′ ⟨_,_⟩₂
+    ; 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)
+
+  βb : ∀ {Γ} → πb ⊚- ∘F ⟨-,-⟩ {Γ} ≃ πʳ
+  βb = pointwise-iso (uncurry β₁b) (uncurry β₂b)
+
+  β : ∀ {Γ} → (πa ⊚- ※ πb ⊚-) ∘F ⟨-,-⟩ {Γ} ≃ idF
+  β = βa ※ⁿⁱ βb
+
+  η : ∀ {Γ} → idF ≃ ⟨-,-⟩ {Γ} ∘F (πa ⊚- ※ πb ⊚-)
+  η = 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 η
+      }
+    }