{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Core using (Category)
module Categories.Category.BinaryProducts {o ℓ e} (𝒞 : Category o ℓ e) where
open import Level hiding (suc)
open import Data.Product using (uncurry)
open Category 𝒞
open HomReasoning
open import Categories.Object.Product 𝒞
open import Categories.Morphism 𝒞 using (_≅_; module Iso; Mono; Epi)
open import Categories.Morphism.Reasoning 𝒞 using (pullʳ; pullˡ; elimʳ; cancelˡ; cancelʳ; introˡ; introʳ)
open import Categories.Category.Monoidal.Core using (Monoidal)
open import Categories.Functor using (Functor) renaming (id to idF)
open import Categories.Functor.Bifunctor using (Bifunctor; appʳ; appˡ)
private
variable
A B C D X Y Z : Obj
f f′ g g′ h i : A ⇒ B
record BinaryProducts : Set (levelOfTerm 𝒞) where
infixr 7 _×_
infixr 8 _⁂_
infix 11 ⟨_,_⟩
field
product : ∀ {A B} → Product A B
private
module product {A} {B} = Product (product {A} {B})
_×_ : Obj → Obj → Obj
A × B = Product.A×B (product {A} {B})
×-comm : A × B ≅ B × A
×-comm = Commutative product product
×-assoc : X × Y × Z ≅ (X × Y) × Z
×-assoc = Associative product product product product
open product hiding (⟨_,_⟩; ∘-distribʳ-⟨⟩) public
⟨_,_⟩ : X ⇒ A → X ⇒ B → X ⇒ A × B
⟨_,_⟩ = Product.⟨_,_⟩ product
_⁂_ : A ⇒ B → C ⇒ D → A × C ⇒ B × D
f ⁂ g = [ product ⇒ product ] f × g
assocˡ : (A × B) × C ⇒ A × B × C
assocˡ = _≅_.to ×-assoc
assocʳ : A × B × C ⇒ (A × B) × C
assocʳ = _≅_.from ×-assoc
assocʳ∘assocˡ : assocʳ {A}{B}{C} ∘ assocˡ {A}{B}{C} ≈ id
assocʳ∘assocˡ = Iso.isoʳ (_≅_.iso ×-assoc)
assocˡ∘assocʳ : assocˡ {A}{B}{C} ∘ assocʳ {A}{B}{C} ≈ id
assocˡ∘assocʳ = Iso.isoˡ (_≅_.iso ×-assoc)
⟨⟩-congʳ : f ≈ f′ → ⟨ f , g ⟩ ≈ ⟨ f′ , g ⟩
⟨⟩-congʳ pf = ⟨⟩-cong₂ pf Equiv.refl
⟨⟩-congˡ : g ≈ g′ → ⟨ f , g ⟩ ≈ ⟨ f , g′ ⟩
⟨⟩-congˡ pf = ⟨⟩-cong₂ Equiv.refl pf
swap : A × B ⇒ B × A
swap = ⟨ π₂ , π₁ ⟩
first : A ⇒ B → A × C ⇒ B × C
first f = f ⁂ id
second : C ⇒ D → A × C ⇒ A × D
second g = id ⁂ g
π₁∘⁂ : π₁ ∘ (f ⁂ g) ≈ f ∘ π₁
π₁∘⁂ {f = f} {g} = project₁
π₂∘⁂ : π₂ ∘ (f ⁂ g) ≈ g ∘ π₂
π₂∘⁂ {f = f} {g} = project₂
⁂-cong₂ : f ≈ g → h ≈ i → f ⁂ h ≈ g ⁂ i
⁂-cong₂ = [ product ⇒ product ]×-cong₂
⁂∘⟨⟩ : (f ⁂ g) ∘ ⟨ f′ , g′ ⟩ ≈ ⟨ f ∘ f′ , g ∘ g′ ⟩
⁂∘⟨⟩ = [ product ⇒ product ]×∘⟨⟩
first∘⟨⟩ : first f ∘ ⟨ f′ , g′ ⟩ ≈ ⟨ f ∘ f′ , g′ ⟩
first∘⟨⟩ = [ product ⇒ product ]×id∘⟨⟩
second∘⟨⟩ : second g ∘ ⟨ f′ , g′ ⟩ ≈ ⟨ f′ , g ∘ g′ ⟩
second∘⟨⟩ = [ product ⇒ product ]id×∘⟨⟩
⁂∘⁂ : (f ⁂ g) ∘ (f′ ⁂ g′) ≈ (f ∘ f′) ⁂ (g ∘ g′)
⁂∘⁂ = [ product ⇒ product ⇒ product ]×∘×
⟨⟩∘ : ⟨ f , g ⟩ ∘ h ≈ ⟨ f ∘ h , g ∘ h ⟩
⟨⟩∘ = [ product ]⟨⟩∘
first∘first : ∀ {C} → first {C = C} f ∘ first g ≈ first (f ∘ g)
first∘first = [ product ⇒ product ⇒ product ]×id∘×id
second∘second : ∀ {A} → second {A = A} f ∘ second g ≈ second (f ∘ g)
second∘second = [ product ⇒ product ⇒ product ]id×∘id×
first∘second : first f ∘ second g ≈ f ⁂ g
first∘second {f = f} {g = g} = begin
first f ∘ second g ≈⟨ first∘⟨⟩ ⟩
⟨ f ∘ id ∘ π₁ , g ∘ π₂ ⟩ ≈⟨ ⟨⟩-congʳ (∘-resp-≈ʳ identityˡ) ⟩
f ⁂ g ∎
second∘first : second f ∘ first g ≈ g ⁂ f
second∘first {f = f} {g = g} = begin
second f ∘ first g ≈⟨ second∘⟨⟩ ⟩
⟨ g ∘ π₁ , f ∘ id ∘ π₂ ⟩ ≈⟨ ⟨⟩-congˡ (∘-resp-≈ʳ identityˡ) ⟩
g ⁂ f ∎
first↔second : first f ∘ second g ≈ second g ∘ first f
first↔second = [ product ⇒ product , product ⇒ product ]first↔second
firstid : ∀ {f : A ⇒ A} (g : A ⇒ C) → first {C = C} f ≈ id → f ≈ id
firstid {f = f} g eq = begin
f ≈˘⟨ elimʳ project₁ ⟩
f ∘ π₁ ∘ ⟨ id , g ⟩ ≈⟨ pullˡ fπ₁≈π₁ ⟩
π₁ ∘ ⟨ id , g ⟩ ≈⟨ project₁ ⟩
id ∎
where fπ₁≈π₁ = begin
f ∘ π₁ ≈˘⟨ project₁ ⟩
π₁ ∘ first f ≈⟨ refl⟩∘⟨ eq ⟩
π₁ ∘ id ≈⟨ identityʳ ⟩
π₁ ∎
swap∘⟨⟩ : swap ∘ ⟨ f , g ⟩ ≈ ⟨ g , f ⟩
swap∘⟨⟩ {f = f} {g = g} = begin
⟨ π₂ , π₁ ⟩ ∘ ⟨ f , g ⟩ ≈⟨ ⟨⟩∘ ⟩
⟨ π₂ ∘ ⟨ f , g ⟩ , π₁ ∘ ⟨ f , g ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ project₂ project₁ ⟩
⟨ g , f ⟩ ∎
swap∘⁂ : swap ∘ (f ⁂ g) ≈ (g ⁂ f) ∘ swap
swap∘⁂ {f = f} {g = g} = begin
swap ∘ (f ⁂ g) ≈⟨ swap∘⟨⟩ ⟩
⟨ g ∘ π₂ , f ∘ π₁ ⟩ ≈˘⟨ ⁂∘⟨⟩ ⟩
(g ⁂ f) ∘ swap ∎
swap∘swap : (swap {A}{B}) ∘ (swap {B}{A}) ≈ id
swap∘swap = Equiv.trans swap∘⟨⟩ η
swap-epi : Epi (swap {A} {B})
swap-epi f g eq = (introʳ swap∘swap) ○ (pullˡ eq) ○ (cancelʳ swap∘swap)
swap-mono : Mono (swap {A} {B})
swap-mono f g eq = (introˡ swap∘swap) ○ (pullʳ eq) ○ (cancelˡ swap∘swap)
assocʳ∘⟨⟩ : assocʳ ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≈ ⟨ ⟨ f , g ⟩ , h ⟩
assocʳ∘⟨⟩ {f = f} {g = g} {h = h} = begin
assocʳ ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≈⟨ ⟨⟩∘ ⟩
⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ ∘ ⟨ f , ⟨ g , h ⟩ ⟩
, (π₂ ∘ π₂) ∘ ⟨ f , ⟨ g , h ⟩ ⟩
⟩ ≈⟨ ⟨⟩-cong₂ ⟨⟩∘ (pullʳ project₂) ⟩
⟨ ⟨ π₁ ∘ ⟨ f , ⟨ g , h ⟩ ⟩
, (π₁ ∘ π₂) ∘ ⟨ f , ⟨ g , h ⟩ ⟩
⟩
, π₂ ∘ ⟨ g , h ⟩
⟩ ≈⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ project₁
(pullʳ project₂ ○ project₁))
project₂ ⟩
⟨ ⟨ f , g ⟩ , h ⟩ ∎
assocˡ∘⟨⟩ : assocˡ ∘ ⟨ ⟨ f , g ⟩ , h ⟩ ≈ ⟨ f , ⟨ g , h ⟩ ⟩
assocˡ∘⟨⟩ {f = f} {g = g} {h = h} = begin
assocˡ ∘ ⟨ ⟨ f , g ⟩ , h ⟩ ≈˘⟨ refl⟩∘⟨ assocʳ∘⟨⟩ ⟩
assocˡ ∘ assocʳ ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≈⟨ cancelˡ assocˡ∘assocʳ ⟩
⟨ f , ⟨ g , h ⟩ ⟩ ∎
assocʳ∘⁂ : assocʳ ∘ (f ⁂ (g ⁂ h)) ≈ ((f ⁂ g) ⁂ h) ∘ assocʳ
assocʳ∘⁂ {f = f} {g = g} {h = h} =
begin
assocʳ ∘ (f ⁂ (g ⁂ h))
≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ⟨⟩∘ ⟩
assocʳ ∘ ⟨ f ∘ π₁ , ⟨ (g ∘ π₁) ∘ π₂ , (h ∘ π₂) ∘ π₂ ⟩ ⟩
≈⟨ assocʳ∘⟨⟩ ⟩
⟨ ⟨ f ∘ π₁ , (g ∘ π₁) ∘ π₂ ⟩ , (h ∘ π₂) ∘ π₂ ⟩
≈⟨ ⟨⟩-cong₂ (⟨⟩-congˡ assoc) assoc ⟩
⟨ ⟨ f ∘ π₁ , g ∘ π₁ ∘ π₂ ⟩ , h ∘ π₂ ∘ π₂ ⟩
≈˘⟨ ⟨⟩-congʳ ⁂∘⟨⟩ ⟩
⟨ (f ⁂ g) ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩ , h ∘ π₂ ∘ π₂ ⟩
≈˘⟨ ⁂∘⟨⟩ ⟩
((f ⁂ g) ⁂ h) ∘ assocʳ
∎
assocˡ∘⁂ : assocˡ ∘ ((f ⁂ g) ⁂ h) ≈ (f ⁂ (g ⁂ h)) ∘ assocˡ
assocˡ∘⁂ {f = f} {g = g} {h = h} =
begin
assocˡ ∘ ((f ⁂ g) ⁂ h)
≈⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟩
assocˡ ∘ ⟨ ⟨ (f ∘ π₁) ∘ π₁ , (g ∘ π₂) ∘ π₁ ⟩ , h ∘ π₂ ⟩
≈⟨ assocˡ∘⟨⟩ ⟩
⟨ (f ∘ π₁) ∘ π₁ , ⟨ (g ∘ π₂) ∘ π₁ , h ∘ π₂ ⟩ ⟩
≈⟨ ⟨⟩-cong₂ assoc (⟨⟩-congʳ assoc) ⟩
⟨ f ∘ π₁ ∘ π₁ , ⟨ g ∘ π₂ ∘ π₁ , h ∘ π₂ ⟩ ⟩
≈˘⟨ ⟨⟩-congˡ ⁂∘⟨⟩ ⟩
⟨ f ∘ π₁ ∘ π₁ , (g ⁂ h) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
≈˘⟨ ⁂∘⟨⟩ ⟩
(f ⁂ (g ⁂ h)) ∘ assocˡ
∎
Δ : ∀ {C} → C ⇒ C × C
Δ {C} = ⟨ id {C} , id ⟩
Δ∘ : Δ ∘ f ≈ ⟨ f , f ⟩
Δ∘ {f = f} = begin
Δ ∘ f ≈⟨ ⟨⟩∘ ⟩
⟨ id ∘ f , id ∘ f ⟩ ≈⟨ ⟨⟩-cong₂ identityˡ identityˡ ⟩
⟨ f , f ⟩ ∎
⁂∘Δ : (f ⁂ g) ∘ Δ ≈ ⟨ f , g ⟩
⁂∘Δ {f = f} {g = g} = begin
(f ⁂ g) ∘ Δ ≈⟨ ⁂∘⟨⟩ ⟩
⟨ f ∘ id , g ∘ id ⟩ ≈⟨ ⟨⟩-cong₂ identityʳ identityʳ ⟩
⟨ f , g ⟩ ∎
-×- : Bifunctor 𝒞 𝒞 𝒞
-×- = record
{ F₀ = uncurry _×_
; F₁ = uncurry _⁂_
; identity = id×id product
; homomorphism = ⟺ ⁂∘⁂
; F-resp-≈ = uncurry [ product ⇒ product ]×-cong₂
}
-×_ : Obj → Functor 𝒞 𝒞
-×_ = appʳ -×-
_×- : Obj → Functor 𝒞 𝒞
_×- = appˡ -×-