{-# OPTIONS --safe #-}
module Cubical.Categories.Category.Precategory where
open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma renaming (_×_ to _×'_)
open import Cubical.Foundations.Pointed hiding (⋆ ; id)
private
variable
ℓ ℓ' : Level
record Precategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
field
ob : Type ℓ
Hom[_,_] : ob → ob → Type ℓ'
id : ∀ {x} → Hom[ x , x ]
_⋆_ : ∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Hom[ x , z ]
⋆IdL : ∀ {x y} (f : Hom[ x , y ]) → id ⋆ f ≡ f
⋆IdR : ∀ {x y} (f : Hom[ x , y ]) → f ⋆ id ≡ f
⋆Assoc : ∀ {u v w x} (f : Hom[ u , v ]) (g : Hom[ v , w ]) (h : Hom[ w , x ])
→ (f ⋆ g) ⋆ h ≡ f ⋆ (g ⋆ h)
_∘_ : ∀ {x y z} (g : Hom[ y , z ]) (f : Hom[ x , y ]) → Hom[ x , z ]
g ∘ f = f ⋆ g
open Precategory
_[_,_] : (C : Precategory ℓ ℓ') → (x y : C .ob) → Type ℓ'
_[_,_] = Hom[_,_]
seq' : ∀ (C : Precategory ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ]
seq' = _⋆_
infixl 15 seq'
syntax seq' C f g = f ⋆⟨ C ⟩ g
comp' : ∀ (C : Precategory ℓ ℓ') {x y z} (g : C [ y , z ]) (f : C [ x , y ]) → C [ x , z ]
comp' = _∘_
infixr 16 comp'
syntax comp' C g f = g ∘⟨ C ⟩ f
record PrecatIso (C : Precategory ℓ ℓ') (x y : C .ob) : Type ℓ' where
constructor precatiso
field
mor : C [ x , y ]
inv : C [ y , x ]
sec : inv ⋆⟨ C ⟩ mor ≡ C .id
ret : mor ⋆⟨ C ⟩ inv ≡ C .id
_^op : Precategory ℓ ℓ' → Precategory ℓ ℓ'
(C ^op) .ob = C .ob
(C ^op) .Hom[_,_] x y = C .Hom[_,_] y x
(C ^op) .id = C .id
(C ^op) ._⋆_ f g = C ._⋆_ g f
(C ^op) .⋆IdL = C .⋆IdR
(C ^op) .⋆IdR = C .⋆IdL
(C ^op) .⋆Assoc f g h = sym (C .⋆Assoc _ _ _)
module _ {ℓC ℓC' : Level} {C : Precategory ℓC ℓC'}
{x y : C .ob} (f : Hom[_,_] C x y) where
record preIsIso : Type (ℓ-max ℓC ℓC') where
field
inv' : Hom[_,_] C y x
sect : _⋆_ C inv' f ≡ id C {y}
retr : _⋆_ C f inv' ≡ id C {x}
open Precategory
open preIsIso
module _ {ℓC ℓC' ℓD ℓD' : Level} where
_×_ : (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD') → Precategory _ _
ob (C × D) = ob C ×' ob D
Hom[_,_] (C × D) (c , d) (c' , d') =
Hom[_,_] C c c' ×' Hom[_,_] D d d'
id (C × D) = id C , id D
_⋆_ (C × D) f g = _⋆_ C (fst f) (fst g) , _⋆_ D (snd f) (snd g)
⋆IdL (C × D) (f , g) i = (⋆IdL C f i) , (⋆IdL D g i)
⋆IdR (C × D) (f , g) i = (⋆IdR C f i) , (⋆IdR D g i)
⋆Assoc (C × D) (f , g) (f' , g') (f'' , g'') i =
⋆Assoc C f f' f'' i , ⋆Assoc D g g' g'' i
record Prefunctor (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD') :
Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
no-eta-equality
field
F-ob : C .ob → D .ob
F-hom : {x y : C .ob} → C [ x , y ] → D [ F-ob x , F-ob y ]
F-id : {x : C .ob} → F-hom {y = x} (id C) ≡ id D
F-seq : {x y z : C .ob} (f : C [ x , y ]) (g : C [ y , z ])
→ F-hom (f ⋆⟨ C ⟩ g) ≡ (F-hom f) ⋆⟨ D ⟩ (F-hom g)
record PreNatTrans (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD')
(F G : Prefunctor C D) :
Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
no-eta-equality
open Prefunctor
field
N-ob : (x : C .ob) → D [ F .F-ob x , G .F-ob x ]
N-hom : {x y : C .ob} (f : C [ x , y ])
→ (F .F-hom f) ⋆⟨ D ⟩ (N-ob y) ≡ (N-ob x) ⋆⟨ D ⟩ (G .F-hom f)
record PreNatIso (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD')
(F G : Prefunctor C D) :
Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
open PreNatTrans
field
trans : PreNatTrans C D F G
isIs : (c : C .ob) → preIsIso {C = D} (trans .N-ob c)
open Prefunctor
open PreNatTrans
open PreNatIso
open preIsIso
module _ {ℓC ℓC' ℓD ℓD' : Level}
{C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'}
(F G H : Prefunctor C D) where
compPreNatTrans : PreNatTrans _ _ F G → PreNatTrans _ _ G H → PreNatTrans _ _ F H
N-ob (compPreNatTrans η γ) c = N-ob η c ⋆⟨ D ⟩ N-ob γ c
N-hom (compPreNatTrans η γ) {x = x} {y = y} f =
sym (⋆Assoc D _ _ _) ∙ cong (λ w → w ⋆⟨ D ⟩ (N-ob γ y)) (N-hom η f)
∙ ⋆Assoc D _ _ _
∙ cong (D ⋆ N-ob η x) (N-hom γ f)
∙ sym (⋆Assoc D _ _ _)
compPreNatIso : PreNatIso _ _ F G → PreNatIso _ _ G H → PreNatIso _ _ F H
trans (compPreNatIso isη isγ) = compPreNatTrans (trans isη) (trans isγ)
inv' (isIs (compPreNatIso isη isγ) c) = inv' (isIs isγ c) ⋆⟨ D ⟩ (inv' (isIs isη c))
sect (isIs (compPreNatIso isη isγ) c) =
⋆Assoc D _ _ _
∙ cong (D ⋆ inv' (isIs isγ c))
(sym (⋆Assoc D _ _ _)
∙ cong (λ w → w ⋆⟨ D ⟩ (N-ob (trans isγ) c)) (sect (isIs isη c))
∙ ⋆IdL D _)
∙ sect (isIs isγ c)
retr (isIs (compPreNatIso isη isγ) c) =
⋆Assoc D _ _ _
∙ cong (D ⋆ N-ob (trans isη) c)
(sym (⋆Assoc D _ _ _)
∙ cong (λ w → w ⋆⟨ D ⟩ (inv' (isIs isη c))) (retr (isIs isγ c))
∙ ⋆IdL D _)
∙ retr (isIs isη c)
module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level}
{C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} {E : Precategory ℓE ℓE'}
where
comp-Prefunctor : (F : Prefunctor C D) (G : Prefunctor D E)
→ Prefunctor C E
F-ob (comp-Prefunctor F G) c = F-ob G (F-ob F c)
F-hom (comp-Prefunctor F G) f = F-hom G (F-hom F f)
F-id (comp-Prefunctor F G) = cong (F-hom G) (F-id F) ∙ F-id G
F-seq (comp-Prefunctor F G) f g = cong (F-hom G) (F-seq F f g) ∙ F-seq G _ _
module _ {ℓC ℓC' : Level} {C : Precategory ℓC ℓC'}
(F : Prefunctor (C × C) C) where
assocₗ : Prefunctor (C × (C × C)) C
F-ob assocₗ (x , y , z) = F-ob F (x , F-ob F (y , z))
F-hom assocₗ {x} {y} (f , g) = F-hom F (f , F-hom F g)
F-id assocₗ =
cong (λ y → F-hom F (id C , y)) (F-id {C = C × C} F)
∙ F-id F
F-seq assocₗ f g =
cong (F-hom F)
(cong (fst (f ⋆⟨ C × (C × C) ⟩ g) ,_)
(F-seq F (snd f) (snd g)))
∙ F-seq F _ _
assocᵣ : Prefunctor (C × (C × C)) C
F-ob assocᵣ (x , y , z) = F-ob F (F-ob F (x , y) , z)
F-hom assocᵣ (f , g) = F-hom F (F-hom F (f , (fst g)) , snd g)
F-id assocᵣ = cong (F-hom F) (cong (_, id C) (F-id F))
∙ F-id F
F-seq assocᵣ (f , f' , f'') (g , g' , g'') =
cong (F-hom F) (cong (_, _⋆_ C f'' g'')
(F-seq F (f , f') (g , g')))
∙ F-seq F _ _
module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level}
{C : Precategory ℓC ℓC'}
{D : Precategory ℓD ℓD'}
{E : Precategory ℓE ℓE'}
where
restrFunctorₗ : (F : Prefunctor (C × D) E) (c : C . ob)
→ Prefunctor D E
F-ob (restrFunctorₗ F c) d = F-ob F (c , d)
F-hom (restrFunctorₗ F c) f = F-hom F (id C , f)
F-id (restrFunctorₗ F c) = F-id F
F-seq (restrFunctorₗ F c) f g =
cong (F-hom F) (ΣPathP (sym (⋆IdR C _) , refl))
∙ F-seq F (id C , f) (id C , g)
restrFunctorᵣ : (F : Prefunctor (C × D) E) (d : D . ob)
→ Prefunctor C E
F-ob (restrFunctorᵣ F d) c = F-ob F (c , d)
F-hom (restrFunctorᵣ F d) f = F-hom F (f , (id D))
F-id (restrFunctorᵣ F d) = F-id F
F-seq (restrFunctorᵣ F d) f g =
cong (F-hom F) (ΣPathP (refl , sym (⋆IdR D _)))
∙ F-seq F (f , id D) (g , id D)
idPrefunctor : {ℓC ℓC' : Level}
(C : Precategory ℓC ℓC')
→ Prefunctor C C
Prefunctor.F-ob (idPrefunctor C) c = c
Prefunctor.F-hom (idPrefunctor C) x = x
Prefunctor.F-id (idPrefunctor C) = refl
Prefunctor.F-seq (idPrefunctor C) _ _ = refl
commFunctor : {ℓC ℓC' ℓD ℓD' : Level}
{C : Precategory ℓC ℓC'}
{D : Precategory ℓD ℓD'}
→ Prefunctor (C × D) (D × C)
Prefunctor.F-ob commFunctor (x , y) = y , x
Prefunctor.F-hom commFunctor (f , g) = g , f
Prefunctor.F-id commFunctor = refl
Prefunctor.F-seq commFunctor _ _ = refl
module _ (M : Precategory ℓ ℓ') where
record isMonoidalPrecategory : Type (ℓ-max ℓ ℓ') where
field
_⊗_ : Prefunctor (M × M) M
𝟙 : ob M
⊗assoc : PreNatIso (M × (M × M)) M (assocₗ _⊗_) (assocᵣ _⊗_)
⊗lUnit : PreNatIso M M (restrFunctorₗ _⊗_ 𝟙) (idPrefunctor M)
⊗rUnit : PreNatIso M M (restrFunctorᵣ _⊗_ 𝟙) (idPrefunctor M)
private
α = N-ob (trans ⊗assoc)
α⁻ : (c : ob M ×' ob M ×' ob M) → M [ _ , _ ]
α⁻ c = preIsIso.inv' (isIs ⊗assoc c)
rId = N-ob (trans ⊗rUnit)
lId = N-ob (trans ⊗lUnit)
field
triang : (a b : M .ob)
→ α (a , 𝟙 , b) ⋆⟨ M ⟩ (F-hom _⊗_ ((rId a) , id M))
≡ F-hom _⊗_ ((id M) , lId b)
⊗pentagon : (a b c d : M .ob)
→ (F-hom _⊗_ (id M , α (b , c , d)))
⋆⟨ M ⟩ ((α (a , (_⊗_ .F-ob (b , c)) , d))
⋆⟨ M ⟩ (F-hom _⊗_ (α (a , b , c) , id M)))
≡ (α (a , b , (F-ob _⊗_ (c , d))))
⋆⟨ M ⟩ (α((F-ob _⊗_ (a , b)) , c , d))
module _ (mon : isMonoidalPrecategory) where
open isMonoidalPrecategory mon
private
α = N-ob (trans ⊗assoc)
α⁻ : (c : ob M ×' ob M ×' ob M) → M [ _ , _ ]
α⁻ c = preIsIso.inv' (isIs ⊗assoc c)
BraidingIsoType : Type _
BraidingIsoType = PreNatIso (M × M) M _⊗_ (comp-Prefunctor commFunctor _⊗_)
HexagonType₁ : (B : BraidingIsoType) → Type _
HexagonType₁ B = (x y z : M .ob) →
F-hom _⊗_ ((id M) , N-ob (trans B) (y , z))
⋆⟨ M ⟩ α (x , z , y)
⋆⟨ M ⟩ F-hom _⊗_ (N-ob (trans B) (x , z) , (id M))
≡ α (x , y , z)
⋆⟨ M ⟩ N-ob (trans B) ((F-ob _⊗_ (x , y)) , z)
⋆⟨ M ⟩ α (z , x , y)
HexagonType₂ : (B : BraidingIsoType) → Type _
HexagonType₂ B = (x y z : M .ob) →
F-hom _⊗_ (N-ob (trans B) (x , y) , id M)
⋆⟨ M ⟩ α⁻ (y , x , z)
⋆⟨ M ⟩ F-hom _⊗_ ((id M) , N-ob (trans B) (x , z))
≡ α⁻ (x , y , z)
⋆⟨ M ⟩ N-ob (trans B) (x , F-ob _⊗_ (y , z))
⋆⟨ M ⟩ α⁻ (y , z , x)
isSymmetricBraiding : (B : BraidingIsoType)
→ Type _
isSymmetricBraiding B = (x y : M .ob) →
N-ob (trans B) (x , y) ⋆⟨ M ⟩ (N-ob (trans B) (y , x))
≡ id M
record isBraidedPrecategory : Type (ℓ-max ℓ ℓ') where
open isMonoidalPrecategory
field
isMonoidal : isMonoidalPrecategory
Braid : BraidingIsoType isMonoidal
hexagons : (x y z : M .ob)
→ HexagonType₁ isMonoidal Braid
×' HexagonType₂ isMonoidal Braid
record isSymmetricPrecategory : Type (ℓ-max ℓ ℓ') where
field
isMonoidal : isMonoidalPrecategory
Braid : BraidingIsoType isMonoidal
hexagon : HexagonType₁ isMonoidal Braid
symBraiding : isSymmetricBraiding isMonoidal Braid
SymmetricMonoidalPrecat : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ'))
SymmetricMonoidalPrecat ℓ ℓ' =
Σ[ C ∈ Precategory ℓ ℓ' ] isSymmetricPrecategory C
module _ (ℓ : Level) where
PointedCat : Precategory (ℓ-suc ℓ) ℓ
ob PointedCat = Pointed ℓ
Hom[_,_] PointedCat A B = A →∙ B
Precategory.id PointedCat = idfun∙ _
_⋆_ PointedCat f g = g ∘∙ f
⋆IdL PointedCat = ∘∙-idˡ
⋆IdR PointedCat = ∘∙-idʳ
⋆Assoc PointedCat f g h = sym (∘∙-assoc h g f)