{-# OPTIONS --without-K --safe #-}
module Categories.Category.Product where
open import Level
open import Function using () renaming (_∘_ to _∙_)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂; zip; map; <_,_>; swap)
open import Categories.Utils.Product
open import Categories.Category using (Category)
open import Categories.Category.Groupoid using (IsGroupoid)
open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation.Core
open import Categories.NaturalTransformation.NaturalIsomorphism hiding (refl)
import Categories.Morphism as Morphism
private
variable
o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ : Level
o₁ ℓ₁ e₁ o′₁ ℓ′₁ e′₁ o₂ ℓ₂ e₂ o′₂ ℓ′₂ e′₂ : Level
C C₁ C₂ D D₁ D₂ : Category o ℓ e
Product : (C : Category o ℓ e) (D : Category o′ ℓ′ e′) → Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
Product C D = record
{ Obj = C.Obj × D.Obj
; _⇒_ = C._⇒_ -< _×_ >- D._⇒_
; _≈_ = C._≈_ -< _×_ >- D._≈_
; _∘_ = zip C._∘_ D._∘_
; id = C.id , D.id
; assoc = C.assoc , D.assoc
; sym-assoc = C.sym-assoc , D.sym-assoc
; identityˡ = C.identityˡ , D.identityˡ
; identityʳ = C.identityʳ , D.identityʳ
; identity² = C.identity² , D.identity²
; equiv = record
{ refl = C.Equiv.refl , D.Equiv.refl
; sym = map C.Equiv.sym D.Equiv.sym
; trans = zip C.Equiv.trans D.Equiv.trans
}
; ∘-resp-≈ = zip C.∘-resp-≈ D.∘-resp-≈
}
where module C = Category C
module D = Category D
infixr 2 _※_
_※_ : ∀ (F : Functor C D₁) → (G : Functor C D₂) → Functor C (Product D₁ D₂)
F ※ G = record
{ F₀ = < F.F₀ , G.F₀ >
; F₁ = < F.F₁ , G.F₁ >
; identity = F.identity , G.identity
; homomorphism = F.homomorphism , G.homomorphism
; F-resp-≈ = < F.F-resp-≈ , G.F-resp-≈ >
}
where module F = Functor F
module G = Functor G
infixr 2 _⁂_
_⁂_ : ∀ (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) → Functor (Product C₁ C₂) (Product D₁ D₂)
F ⁂ G = record
{ F₀ = map F.F₀ G.F₀
; F₁ = map F.F₁ G.F₁
; identity = F.identity , G.identity
; homomorphism = F.homomorphism , G.homomorphism
; F-resp-≈ = map F.F-resp-≈ G.F-resp-≈
}
where module F = Functor F
module G = Functor G
infixr 5 _⁂ⁿ_
_⁂ⁿ_ : ∀ {C₁ : Category o₁ ℓ₁ e₁} {D₁ : Category o′₁ ℓ′₁ e′₁}
{C₂ : Category o₂ ℓ₂ e₂} {D₂ : Category o′₂ ℓ′₂ e′₂}
{F₁ G₁ : Functor C₁ D₁} {F₂ G₂ : Functor C₂ D₂}
(α : NaturalTransformation F₁ G₁) (β : NaturalTransformation F₂ G₂) →
NaturalTransformation (F₁ ⁂ F₂) (G₁ ⁂ G₂)
α ⁂ⁿ β = ntHelper record
{ η = map⁎′ α.η β.η
; commute = map⁎′ α.commute β.commute
}
where module α = NaturalTransformation α
module β = NaturalTransformation β
infixr 5 _※ⁿ_
_※ⁿ_ : ∀ {D₁ : Category o ℓ e} {D₂ : Category o′ ℓ′ e′}
{F₁ G₁ : Functor C D₁} {F₂ G₂ : Functor C D₂}
(α : NaturalTransformation F₁ G₁) →
(β : NaturalTransformation F₂ G₂) →
NaturalTransformation (F₁ ※ F₂) (G₁ ※ G₂)
α ※ⁿ β = ntHelper record
{ η = < α.η , β.η >
; commute = < α.commute , β.commute >
}
where module α = NaturalTransformation α
module β = NaturalTransformation β
infixr 5 _⁂ⁿⁱ_
_⁂ⁿⁱ_ : ∀ {C₁ : Category o₁ ℓ₁ e₁} {D₁ : Category o′₁ ℓ′₁ e′₁}
{C₂ : Category o₂ ℓ₂ e₂} {D₂ : Category o′₂ ℓ′₂ e′₂}
{F₁ G₁ : Functor C₁ D₁} {F₂ G₂ : Functor C₂ D₂}
(α : NaturalIsomorphism F₁ G₁) (β : NaturalIsomorphism F₂ G₂) →
NaturalIsomorphism (F₁ ⁂ F₂) (G₁ ⁂ G₂)
α ⁂ⁿⁱ β = record
{ F⇒G = α.F⇒G ⁂ⁿ β.F⇒G
; F⇐G = α.F⇐G ⁂ⁿ β.F⇐G
; iso = λ where
(X , Y) → record
{ isoˡ = isoˡ (α.iso X) , isoˡ (β.iso Y)
; isoʳ = isoʳ (α.iso X) , isoʳ (β.iso Y)
}
}
where module α = NaturalIsomorphism α
module β = NaturalIsomorphism β
open Morphism.Iso
infixr 5 _※ⁿⁱ_
_※ⁿⁱ_ : ∀ {D₁ : Category o ℓ e} {D₂ : Category o′ ℓ′ e′}
{F₁ G₁ : Functor C D₁} {F₂ G₂ : Functor C D₂}
(α : NaturalIsomorphism F₁ G₁) →
(β : NaturalIsomorphism F₂ G₂) →
NaturalIsomorphism (F₁ ※ F₂) (G₁ ※ G₂)
α ※ⁿⁱ β = record
{ F⇒G = α.F⇒G ※ⁿ β.F⇒G
; F⇐G = α.F⇐G ※ⁿ β.F⇐G
; iso = λ X → record
{ isoˡ = isoˡ (α.iso X) , isoˡ (β.iso X)
; isoʳ = isoʳ (α.iso X) , isoʳ (β.iso X)
}
}
where module α = NaturalIsomorphism α
module β = NaturalIsomorphism β
open Morphism.Iso
module _ (C₁ : Category o ℓ e) (C₂ : Category o′ ℓ′ e′) (C₃ : Category o″ ℓ″ e″) where
private
module C₁ = Category C₁
module C₂ = Category C₂
module C₃ = Category C₃
assocˡ : Functor (Product (Product C₁ C₂) C₃) (Product C₁ (Product C₂ C₃))
assocˡ = record
{ F₀ = < proj₁ ∙ proj₁ , < proj₂ ∙ proj₁ , proj₂ > >
; F₁ = < proj₁ ∙ proj₁ , < proj₂ ∙ proj₁ , proj₂ > >
; identity = C₁.Equiv.refl , C₂.Equiv.refl , C₃.Equiv.refl
; homomorphism = C₁.Equiv.refl , C₂.Equiv.refl , C₃.Equiv.refl
; F-resp-≈ = < proj₁ ∙ proj₁ , < proj₂ ∙ proj₁ , proj₂ > >
}
assocʳ : Functor (Product C₁ (Product C₂ C₃)) (Product (Product C₁ C₂) C₃)
assocʳ = record
{ F₀ = < < proj₁ , proj₁ ∙ proj₂ > , proj₂ ∙ proj₂ >
; F₁ = < < proj₁ , proj₁ ∙ proj₂ > , proj₂ ∙ proj₂ >
; identity = (C₁.Equiv.refl , C₂.Equiv.refl) , C₃.Equiv.refl
; homomorphism = (C₁.Equiv.refl , C₂.Equiv.refl) , C₃.Equiv.refl
; F-resp-≈ = < < proj₁ , proj₁ ∙ proj₂ > , proj₂ ∙ proj₂ >
}
module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} where
private
module C = Category C
module D = Category D
πˡ : Functor (Product C D) C
πˡ = record
{ F₀ = proj₁
; F₁ = proj₁
; identity = refl
; homomorphism = refl
; F-resp-≈ = proj₁
}
where open C.Equiv using (refl)
πʳ : Functor (Product C D) D
πʳ = record
{ F₀ = proj₂
; F₁ = proj₂
; identity = refl
; homomorphism = refl
; F-resp-≈ = proj₂
}
where open D.Equiv using (refl)
Swap : Functor (Product C D) (Product D C)
Swap = record
{ F₀ = swap
; F₁ = swap
; identity = D.Equiv.refl , C.Equiv.refl
; homomorphism = D.Equiv.refl , C.Equiv.refl
; F-resp-≈ = swap
}
Groupoid-× : {C : Category o₁ ℓ₁ e₁} {D : Category o₂ ℓ₂ e₂}
→ IsGroupoid C → IsGroupoid D → IsGroupoid (Product C D)
Groupoid-× c₁ c₂ = record
{ _⁻¹ = map (IsGroupoid._⁻¹ c₁) (IsGroupoid._⁻¹ c₂)
; iso = record { isoˡ = Iso.isoˡ i₁ , Iso.isoˡ i₂
; isoʳ = Iso.isoʳ i₁ , Iso.isoʳ i₂
}
}
where
open Morphism
i₁ = IsGroupoid.iso c₁
i₂ = IsGroupoid.iso c₂