From d182af36a763d0a354f83650a44e5ac8d5c9726f Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Wed, 21 Feb 2024 10:02:27 +0100 Subject: [PATCH] move precategories to separate folder and rename to wild categories (#1103) * introduce wild categories, copying from precategories refactor (split into files) rename add instance for Types * split further * define univalence, fix things * add path category * refactor use case * remove now obsolete precategory * update refs in Papers * move instance (of WildCat) * rename * remove duplication --- Cubical/Categories/Category/Precategory.agda | 338 ------------------ Cubical/Categories/Instances/Categories.agda | 25 -- .../Categories/Instances/TypePrecategory.agda | 19 - .../HITs/SmashProduct/SymmetricMonoidal.agda | 85 +---- .../SmashProduct/SymmetricMonoidalCat.agda | 96 +++++ Cubical/Papers/SmashProducts.agda | 16 +- Cubical/README.agda | 3 + Cubical/WildCat/Base.agda | 88 +++++ Cubical/WildCat/BraidedSymmetricMonoidal.agda | 109 ++++++ Cubical/WildCat/Functor.agda | 164 +++++++++ Cubical/WildCat/Instances/Categories.agda | 26 ++ Cubical/WildCat/Instances/Path.agda | 22 ++ Cubical/WildCat/Instances/Pointed.agda | 18 + Cubical/WildCat/Instances/Types.agda | 19 + Cubical/WildCat/Product.agda | 26 ++ 15 files changed, 586 insertions(+), 468 deletions(-) delete mode 100644 Cubical/Categories/Category/Precategory.agda delete mode 100644 Cubical/Categories/Instances/Categories.agda delete mode 100644 Cubical/Categories/Instances/TypePrecategory.agda create mode 100644 Cubical/HITs/SmashProduct/SymmetricMonoidalCat.agda create mode 100644 Cubical/WildCat/Base.agda create mode 100644 Cubical/WildCat/BraidedSymmetricMonoidal.agda create mode 100644 Cubical/WildCat/Functor.agda create mode 100644 Cubical/WildCat/Instances/Categories.agda create mode 100644 Cubical/WildCat/Instances/Path.agda create mode 100644 Cubical/WildCat/Instances/Pointed.agda create mode 100644 Cubical/WildCat/Instances/Types.agda create mode 100644 Cubical/WildCat/Product.agda diff --git a/Cubical/Categories/Category/Precategory.agda b/Cubical/Categories/Category/Precategory.agda deleted file mode 100644 index 7c4eb3d6d5..0000000000 --- a/Cubical/Categories/Category/Precategory.agda +++ /dev/null @@ -1,338 +0,0 @@ -{-# 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 - --- Precategories -record Precategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where - -- no-eta-equality ; NOTE: need eta equality for `opop` - 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) - - -- composition: alternative to diagramatic order - _∘_ : ∀ {x y z} (g : Hom[ y , z ]) (f : Hom[ x , y ]) → Hom[ x , z ] - g ∘ f = f ⋆ g - -open Precategory - --- Helpful syntax/notation -_[_,_] : (C : Precategory ℓ ℓ') → (x y : C .ob) → Type ℓ' -_[_,_] = Hom[_,_] - --- Needed to define this in order to be able to make the subsequence syntax declaration -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 - --- composition -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 - --- Isomorphisms and paths in precategories -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 - --- Opposite precategory -_^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 _ _ _) - --- Natural isomorphisms -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 - -- Products - _×_ : (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 - - -- Functors - 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) - - -- Natural transformation - 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) - - -- Natural isomorphisms - 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 _ _ - --- Left and right restrictions of functors -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) - --- Identity functor -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 - --- Commutator -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 - --- Monoidal, braided and monoidal symmetric precategories -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 - -- Note: associators are on the form x ⊗ (y ⊗ z) → (x ⊗ y) ⊗ z - 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 - --- Instances -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) diff --git a/Cubical/Categories/Instances/Categories.agda b/Cubical/Categories/Instances/Categories.agda deleted file mode 100644 index 7ce6b89a2f..0000000000 --- a/Cubical/Categories/Instances/Categories.agda +++ /dev/null @@ -1,25 +0,0 @@ --- The (pre)category of (small) categories -{-# OPTIONS --safe #-} - -module Cubical.Categories.Instances.Categories where - -open import Cubical.Categories.Category.Base -open import Cubical.Categories.Category.Precategory -open import Cubical.Categories.Functor.Base -open import Cubical.Categories.Functor.Properties -open import Cubical.Foundations.Prelude - - -module _ (ℓ ℓ' : Level) where - open Precategory - - CatPrecategory : Precategory (ℓ-suc (ℓ-max ℓ ℓ')) (ℓ-max ℓ ℓ') - CatPrecategory .ob = Category ℓ ℓ' - CatPrecategory .Hom[_,_] = Functor - CatPrecategory .id = 𝟙⟨ _ ⟩ - CatPrecategory ._⋆_ G H = H ∘F G - CatPrecategory .⋆IdL _ = F-lUnit - CatPrecategory .⋆IdR _ = F-rUnit - CatPrecategory .⋆Assoc _ _ _ = F-assoc - --- TODO: what is required for Functor C D to be a set? diff --git a/Cubical/Categories/Instances/TypePrecategory.agda b/Cubical/Categories/Instances/TypePrecategory.agda deleted file mode 100644 index 41f62ef709..0000000000 --- a/Cubical/Categories/Instances/TypePrecategory.agda +++ /dev/null @@ -1,19 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Categories.Instances.TypePrecategory where - -open import Cubical.Foundations.Prelude - -open import Cubical.Categories.Category.Precategory - -open Precategory - --- TYPE precategory has types as objects -module _ ℓ where - TYPE : Precategory (ℓ-suc ℓ) ℓ - TYPE .ob = Type ℓ - TYPE .Hom[_,_] A B = A → B - TYPE .id = λ x → x - TYPE ._⋆_ f g = λ x → g (f x) - TYPE .⋆IdL f = refl - TYPE .⋆IdR f = refl - TYPE .⋆Assoc f g h = refl diff --git a/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda b/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda index 900b5fd7fc..1214b95c17 100644 --- a/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda +++ b/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda @@ -1,42 +1,23 @@ {-# OPTIONS --safe #-} - -{- -This file contians a proof that the smash product turns the universe -of pointed types into a symmetric monoidal precategory. The pentagon -and hexagon are proved in separate files due to the length of the -proofs. The remaining identities and the main result are proved here. --} - module Cubical.HITs.SmashProduct.SymmetricMonoidal where -open import Cubical.HITs.SmashProduct.Base open import Cubical.Foundations.Prelude open import Cubical.Foundations.Pointed open import Cubical.Foundations.Isomorphism -open import Cubical.HITs.Pushout.Base -open import Cubical.Data.Unit -open import Cubical.Data.Sigma -open import Cubical.HITs.Wedge open import Cubical.Foundations.GroupoidLaws open import Cubical.Foundations.Pointed.Homogeneous open import Cubical.Foundations.Path open import Cubical.Foundations.Function open import Cubical.Foundations.Equiv + +open import Cubical.Data.Unit +open import Cubical.Data.Sigma +open import Cubical.Data.Bool +open import Cubical.HITs.Wedge +open import Cubical.HITs.Pushout.Base open import Cubical.HITs.SmashProduct.Base open import Cubical.HITs.SmashProduct.Pentagon open import Cubical.HITs.SmashProduct.Hexagon -open import Cubical.Categories.Category.Precategory - renaming (_×_ to _×'_) -open import Cubical.Data.Bool - -open Precategory hiding (_∘_) -open Prefunctor -open isSymmetricPrecategory -open isMonoidalPrecategory -open PreNatIso -open PreNatTrans -open preIsIso - private variable @@ -527,57 +508,3 @@ snd ⋀lIdEquiv∙ = refl cong (push (inl (snd A)) ∙_) (sym (rUnit _) ∙ (λ i j → push (push tt (~ i)) (~ j))) ∙ rCancel _ - - --- ⋀ as a functor -⋀F : ∀ {ℓ} → Prefunctor (PointedCat ℓ ×' PointedCat ℓ) (PointedCat ℓ) -F-ob ⋀F (A , B) = A ⋀∙ B -F-hom ⋀F (f , g) = f ⋀→∙ g -F-id ⋀F = ⋀→∙-idfun -F-seq ⋀F (f , g) (f' , g') = ⋀→∙-comp f f' g g' - -⋀lUnitNatIso : PreNatIso (PointedCat ℓ) (PointedCat ℓ) - (restrFunctorₗ ⋀F Bool*∙) (idPrefunctor (PointedCat ℓ)) -N-ob (trans ⋀lUnitNatIso) X = ≃∙map ⋀lIdEquiv∙ -N-hom (trans ⋀lUnitNatIso) f = ⋀lId-sq f -inv' (isIs ⋀lUnitNatIso c) = ≃∙map (invEquiv∙ ⋀lIdEquiv∙) -sect (isIs (⋀lUnitNatIso {ℓ = ℓ}) c) = - ≃∙→ret/sec∙ (⋀lIdEquiv∙ {ℓ = ℓ} {A = c}) .snd -retr (isIs ⋀lUnitNatIso c) = - ≃∙→ret/sec∙ ⋀lIdEquiv∙ .fst - -makeIsIso-Pointed : ∀ {ℓ} {A B : Pointed ℓ} {f : A →∙ B} - → isEquiv (fst f) → preIsIso {C = PointedCat ℓ} f -inv' (makeIsIso-Pointed {f = f} eq) = ≃∙map (invEquiv∙ ((fst f , eq) , snd f)) -sect (makeIsIso-Pointed {f = f} eq) = ≃∙→ret/sec∙ ((fst f , eq) , snd f) .snd -retr (makeIsIso-Pointed {f = f} eq) = ≃∙→ret/sec∙ ((fst f , eq) , snd f) .fst - -restrₗᵣ : PreNatIso (PointedCat ℓ) (PointedCat ℓ) - (restrFunctorᵣ ⋀F Bool*∙) (restrFunctorₗ ⋀F Bool*∙) -N-ob (trans restrₗᵣ) X = ⋀comm→∙ -N-hom (trans restrₗᵣ) f = ⋀comm-sq f (idfun∙ Bool*∙) -isIs restrₗᵣ c = makeIsIso-Pointed (isoToIsEquiv ⋀CommIso) - --- main result -⋀Symm : ∀ {ℓ} → isSymmetricPrecategory (PointedCat ℓ) -_⊗_ (isMonoidal ⋀Symm) = ⋀F -𝟙 (isMonoidal ⋀Symm) = Bool*∙ -N-ob (trans (⊗assoc (isMonoidal ⋀Symm))) (A , B , C) = ≃∙map SmashAssocEquiv∙ -N-hom (trans (⊗assoc (isMonoidal ⋀Symm))) (f , g , h) = ⋀assoc-⋀→∙ f g h -inv' (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) = - ≃∙map (invEquiv∙ SmashAssocEquiv∙) -sect (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) = - ≃∙→ret/sec∙ SmashAssocEquiv∙ .snd -retr (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) = - ≃∙→ret/sec∙ SmashAssocEquiv∙ .fst -⊗lUnit (isMonoidal ⋀Symm) = ⋀lUnitNatIso -⊗rUnit (isMonoidal ⋀Symm) = compPreNatIso _ _ _ restrₗᵣ ⋀lUnitNatIso -triang (isMonoidal (⋀Symm {ℓ})) X Y = ⋀triang -⊗pentagon (isMonoidal ⋀Symm) X Y Z W = - (∘∙-assoc assc₅∙ assc₄∙ assc₃∙) ∙ pentagon∙ -N-ob (trans (Braid ⋀Symm)) X = ⋀comm→∙ -N-hom (trans (Braid ⋀Symm)) (f , g) = ⋀comm-sq f g -isIs (Braid ⋀Symm) _ = makeIsIso-Pointed (isoToIsEquiv ⋀CommIso) -isSymmetricPrecategory.hexagon ⋀Symm a b c = hexagon∙ -symBraiding ⋀Symm X Y = - ΣPathP ((funExt (Iso.rightInv ⋀CommIso)) , (sym (rUnit refl))) diff --git a/Cubical/HITs/SmashProduct/SymmetricMonoidalCat.agda b/Cubical/HITs/SmashProduct/SymmetricMonoidalCat.agda new file mode 100644 index 0000000000..89926be7ae --- /dev/null +++ b/Cubical/HITs/SmashProduct/SymmetricMonoidalCat.agda @@ -0,0 +1,96 @@ +{-# OPTIONS --safe #-} + +{- +This file contians a proof that the smash product turns the universe +of pointed types into a symmetric monoidal wild category. The pentagon +and hexagon are proved in separate files due to the length of the +proofs. The remaining identities and the main result are proved here. +-} + +module Cubical.HITs.SmashProduct.SymmetricMonoidalCat where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Path +open import Cubical.Foundations.Equiv + +open import Cubical.Data.Unit +open import Cubical.Data.Sigma using (ΣPathP) +open import Cubical.Data.Bool +open import Cubical.HITs.SmashProduct.Base +open import Cubical.HITs.SmashProduct.Pentagon +open import Cubical.HITs.SmashProduct.Hexagon +open import Cubical.HITs.SmashProduct.SymmetricMonoidal + +open import Cubical.WildCat.Base +open import Cubical.WildCat.Functor +open import Cubical.WildCat.Product +open import Cubical.WildCat.BraidedSymmetricMonoidal +open import Cubical.WildCat.Instances.Pointed + +open WildCat +open WildFunctor +open isSymmetricWildCat +open isMonoidalWildCat +open WildNatIso +open WildNatTrans +open wildIsIso + +private + variable + ℓ ℓ' : Level + +-- ⋀ as a functor +⋀F : ∀ {ℓ} → WildFunctor (PointedCat ℓ × PointedCat ℓ) (PointedCat ℓ) +F-ob ⋀F (A , B) = A ⋀∙ B +F-hom ⋀F (f , g) = f ⋀→∙ g +F-id ⋀F = ⋀→∙-idfun +F-seq ⋀F (f , g) (f' , g') = ⋀→∙-comp f f' g g' + +⋀lUnitNatIso : WildNatIso (PointedCat ℓ) (PointedCat ℓ) + (restrFunctorₗ ⋀F Bool*∙) (idWildFunctor (PointedCat ℓ)) +N-ob (trans ⋀lUnitNatIso) X = ≃∙map ⋀lIdEquiv∙ +N-hom (trans ⋀lUnitNatIso) f = ⋀lId-sq f +inv' (isIs ⋀lUnitNatIso c) = ≃∙map (invEquiv∙ ⋀lIdEquiv∙) +sect (isIs (⋀lUnitNatIso {ℓ = ℓ}) c) = + ≃∙→ret/sec∙ (⋀lIdEquiv∙ {ℓ = ℓ} {A = c}) .snd +retr (isIs ⋀lUnitNatIso c) = + ≃∙→ret/sec∙ ⋀lIdEquiv∙ .fst + +makeIsIso-Pointed : ∀ {ℓ} {A B : Pointed ℓ} {f : A →∙ B} + → isEquiv (fst f) → wildIsIso {C = PointedCat ℓ} f +inv' (makeIsIso-Pointed {f = f} eq) = ≃∙map (invEquiv∙ ((fst f , eq) , snd f)) +sect (makeIsIso-Pointed {f = f} eq) = ≃∙→ret/sec∙ ((fst f , eq) , snd f) .snd +retr (makeIsIso-Pointed {f = f} eq) = ≃∙→ret/sec∙ ((fst f , eq) , snd f) .fst + +restrₗᵣ : WildNatIso (PointedCat ℓ) (PointedCat ℓ) + (restrFunctorᵣ ⋀F Bool*∙) (restrFunctorₗ ⋀F Bool*∙) +N-ob (trans restrₗᵣ) X = ⋀comm→∙ +N-hom (trans restrₗᵣ) f = ⋀comm-sq f (idfun∙ Bool*∙) +isIs restrₗᵣ c = makeIsIso-Pointed (isoToIsEquiv ⋀CommIso) + +-- main result +⋀Symm : ∀ {ℓ} → isSymmetricWildCat (PointedCat ℓ) +_⊗_ (isMonoidal ⋀Symm) = ⋀F +𝟙 (isMonoidal ⋀Symm) = Bool*∙ +N-ob (trans (⊗assoc (isMonoidal ⋀Symm))) (A , B , C) = ≃∙map SmashAssocEquiv∙ +N-hom (trans (⊗assoc (isMonoidal ⋀Symm))) (f , g , h) = ⋀assoc-⋀→∙ f g h +inv' (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) = + ≃∙map (invEquiv∙ SmashAssocEquiv∙) +sect (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) = + ≃∙→ret/sec∙ SmashAssocEquiv∙ .snd +retr (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) = + ≃∙→ret/sec∙ SmashAssocEquiv∙ .fst +⊗lUnit (isMonoidal ⋀Symm) = ⋀lUnitNatIso +⊗rUnit (isMonoidal ⋀Symm) = compWildNatIso _ _ _ restrₗᵣ ⋀lUnitNatIso +triang (isMonoidal (⋀Symm {ℓ})) X Y = ⋀triang +⊗pentagon (isMonoidal ⋀Symm) X Y Z W = + (∘∙-assoc assc₅∙ assc₄∙ assc₃∙) ∙ pentagon∙ +N-ob (trans (Braid ⋀Symm)) X = ⋀comm→∙ +N-hom (trans (Braid ⋀Symm)) (f , g) = ⋀comm-sq f g +isIs (Braid ⋀Symm) _ = makeIsIso-Pointed (isoToIsEquiv ⋀CommIso) +isSymmetricWildCat.hexagon ⋀Symm a b c = hexagon∙ +symBraiding ⋀Symm X Y = + ΣPathP ((funExt (Iso.rightInv ⋀CommIso)) , (sym (rUnit refl))) diff --git a/Cubical/Papers/SmashProducts.agda b/Cubical/Papers/SmashProducts.agda index 3ee0edf037..25aa062464 100644 --- a/Cubical/Papers/SmashProducts.agda +++ b/Cubical/Papers/SmashProducts.agda @@ -14,14 +14,16 @@ Axel Ljungström, 2024 {-# OPTIONS --safe #-} module Cubical.Papers.SmashProducts where -- Section 2 -import Cubical.Categories.Category.Precategory as WCat +import Cubical.WildCat.Base as WCat1 +import Cubical.WildCat.Instances.Pointed as WCat2 +import Cubical.WildCat.BraidedSymmetricMonoidal as WCat3 import Cubical.HITs.SmashProduct.Base as Smash -- Section 3 import Cubical.Foundations.Pointed.Homogeneous as Hom -- Section 5 -import Cubical.HITs.SmashProduct.SymmetricMonoidal as SM +import Cubical.HITs.SmashProduct.SymmetricMonoidalCat as SM -- Section 6 import Cubical.HITs.SmashProduct.Induction as SmashInduction @@ -29,17 +31,17 @@ import Cubical.HITs.SmashProduct.Induction as SmashInduction ---- 2 Background ---- --- 2.1 Symmetric monoidal wild categories --- Definition 1 (Wild categories - note: currently called precategories in the library) -open WCat using (Precategory) +-- Definition 1 (Wild categories) +open WCat1 using (WildCat) -- Proposition 2 (Pointed types form a wild cat) -open WCat using (PointedCat) +open WCat2 using (PointedCat) -- Definition 3 (Monoidal wild categories) -open WCat using (isMonoidalPrecategory) +open WCat3 using (isMonoidalWildCat) -- Definition 4 (Symmetric Monoidal wild categories) -open WCat using (SymmetricMonoidalPrecat) +open WCat3 using (SymmetricMonoidalPrecat) --- 2.2 Smash Products -- Definition 5 (Smash products -- note: defined as a coproduct in the diff --git a/Cubical/README.agda b/Cubical/README.agda index c1f7d002fa..ed23331c73 100644 --- a/Cubical/README.agda +++ b/Cubical/README.agda @@ -40,6 +40,9 @@ import Cubical.Papers.Everything -- Properties and proofs about relations import Cubical.Relation.Everything +-- Wild category theory +import Cubical.WildCat.Everything + -- Category theory import Cubical.Categories.Everything diff --git a/Cubical/WildCat/Base.agda b/Cubical/WildCat/Base.agda new file mode 100644 index 0000000000..fca6167fe7 --- /dev/null +++ b/Cubical/WildCat/Base.agda @@ -0,0 +1,88 @@ +{- + wild categories, analogous to the formalization in Coq-HoTT + + https://github.com/HoTT/Coq-HoTT/tree/master/theories/WildCat + +-} +{-# OPTIONS --safe #-} +module Cubical.WildCat.Base where + +open import Cubical.Foundations.Prelude + +open import Cubical.Data.Sigma renaming (_×_ to _×'_) + +private + variable + ℓ ℓ' : Level + +record WildCat ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where + no-eta-equality + 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) + + -- composition: alternative to diagramatic order + _∘_ : ∀ {x y z} (g : Hom[ y , z ]) (f : Hom[ x , y ]) → Hom[ x , z ] + g ∘ f = f ⋆ g + +open WildCat + +-- Helpful syntax/notation +_[_,_] : (C : WildCat ℓ ℓ') → (x y : C .ob) → Type ℓ' +_[_,_] = Hom[_,_] + +-- Needed to define this in order to be able to make the subsequence syntax declaration +seq' : ∀ (C : WildCat ℓ ℓ') {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 + +-- composition +comp' : ∀ (C : WildCat ℓ ℓ') {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 + +-- Isomorphisms in wild categories (analogous to HoTT-terminology for maps between types) +record WildCatIso (C : WildCat ℓ ℓ') (x y : C .ob) : Type ℓ' where + no-eta-equality + constructor wildiso + field + mor : C [ x , y ] + inv : C [ y , x ] + sec : inv ⋆⟨ C ⟩ mor ≡ C .id + ret : mor ⋆⟨ C ⟩ inv ≡ C .id + +idIso : {C : WildCat ℓ ℓ'} {x : C .ob} → WildCatIso C x x +idIso {C = C} = wildiso (C .id ) (C .id) (C .⋆IdL (C .id)) (C .⋆IdL (C .id)) + +pathToIso : {C : WildCat ℓ ℓ'} {x y : C .ob} (p : x ≡ y) → WildCatIso C x y +pathToIso {C = C} p = J (λ z _ → WildCatIso C _ z) idIso p + +-- Natural isomorphisms +module _ {C : WildCat ℓ ℓ'} + {x y : C .ob} (f : Hom[_,_] C x y) where + record wildIsIso : Type (ℓ-max ℓ ℓ') where + no-eta-equality + field + inv' : Hom[_,_] C y x + sect : _⋆_ C inv' f ≡ id C {y} + retr : _⋆_ C f inv' ≡ id C {x} + +-- Opposite wild category +_^op : WildCat ℓ ℓ' → WildCat ℓ ℓ' +(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 _ _ _) diff --git a/Cubical/WildCat/BraidedSymmetricMonoidal.agda b/Cubical/WildCat/BraidedSymmetricMonoidal.agda new file mode 100644 index 0000000000..7f0287332d --- /dev/null +++ b/Cubical/WildCat/BraidedSymmetricMonoidal.agda @@ -0,0 +1,109 @@ +{- + Monoidal, braided and monoidal symmetric wild categories +-} +{-# OPTIONS --safe #-} +module Cubical.WildCat.BraidedSymmetricMonoidal where + +open import Cubical.Foundations.Prelude + +open import Cubical.Data.Sigma renaming (_×_ to _×'_) + +open import Cubical.WildCat.Base +open import Cubical.WildCat.Product +open import Cubical.WildCat.Functor + +private + variable + ℓ ℓ' : Level + +open WildCat + +open WildFunctor +open WildNatTrans +open WildNatIso +open wildIsIso + +module _ (M : WildCat ℓ ℓ') where + record isMonoidalWildCat : Type (ℓ-max ℓ ℓ') where + field + _⊗_ : WildFunctor (M × M) M + 𝟙 : ob M + + ⊗assoc : WildNatIso (M × (M × M)) M (assocₗ _⊗_) (assocᵣ _⊗_) + + ⊗lUnit : WildNatIso M M (restrFunctorₗ _⊗_ 𝟙) (idWildFunctor M) + ⊗rUnit : WildNatIso M M (restrFunctorᵣ _⊗_ 𝟙) (idWildFunctor M) + + private + α = N-ob (trans ⊗assoc) + α⁻ : (c : ob M ×' ob M ×' ob M) → M [ _ , _ ] + α⁻ c = wildIsIso.inv' (isIs ⊗assoc c) + rId = N-ob (trans ⊗rUnit) + lId = N-ob (trans ⊗lUnit) + + field + -- Note: associators are on the form x ⊗ (y ⊗ z) → (x ⊗ y) ⊗ z + 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 : isMonoidalWildCat) where + open isMonoidalWildCat mon + private + α = N-ob (trans ⊗assoc) + α⁻ : (c : ob M ×' ob M ×' ob M) → M [ _ , _ ] + α⁻ c = wildIsIso.inv' (isIs ⊗assoc c) + + BraidingIsoType : Type _ + BraidingIsoType = WildNatIso (M × M) M _⊗_ (comp-WildFunctor 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 isBraidedWildCat : Type (ℓ-max ℓ ℓ') where + open isMonoidalWildCat + field + isMonoidal : isMonoidalWildCat + Braid : BraidingIsoType isMonoidal + hexagons : (x y z : M .ob) + → HexagonType₁ isMonoidal Braid + ×' HexagonType₂ isMonoidal Braid + + record isSymmetricWildCat : Type (ℓ-max ℓ ℓ') where + field + isMonoidal : isMonoidalWildCat + Braid : BraidingIsoType isMonoidal + hexagon : HexagonType₁ isMonoidal Braid + symBraiding : isSymmetricBraiding isMonoidal Braid + +SymmetricMonoidalPrecat : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ')) +SymmetricMonoidalPrecat ℓ ℓ' = + Σ[ C ∈ WildCat ℓ ℓ' ] isSymmetricWildCat C diff --git a/Cubical/WildCat/Functor.agda b/Cubical/WildCat/Functor.agda new file mode 100644 index 0000000000..352a3a0fff --- /dev/null +++ b/Cubical/WildCat/Functor.agda @@ -0,0 +1,164 @@ +{-# OPTIONS --safe #-} +module Cubical.WildCat.Functor where + +open import Cubical.Foundations.Prelude + +open import Cubical.Data.Sigma using (ΣPathP) + +open import Cubical.WildCat.Base +open import Cubical.WildCat.Product + +open WildCat + +private + variable + ℓ ℓ' : Level + ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level + + -- Functors +record WildFunctor (C : WildCat ℓC ℓC') (D : WildCat ℓ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) + +-- Natural transformation +record WildNatTrans (C : WildCat ℓC ℓC') (D : WildCat ℓD ℓD') + (F G : WildFunctor C D) : + Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where + no-eta-equality + + open WildFunctor + + 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) + +-- Natural isomorphisms +record WildNatIso (C : WildCat ℓC ℓC') (D : WildCat ℓD ℓD') + (F G : WildFunctor C D) : + Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where + open WildNatTrans + + field + trans : WildNatTrans C D F G + isIs : (c : C .ob) → wildIsIso {C = D} (trans .N-ob c) + +open WildFunctor +open WildNatTrans +open WildNatIso +open wildIsIso + +module _ + {C : WildCat ℓC ℓC'} {D : WildCat ℓD ℓD'} + (F G H : WildFunctor C D) where + + compWildNatTrans : WildNatTrans _ _ F G → WildNatTrans _ _ G H → WildNatTrans _ _ F H + N-ob (compWildNatTrans η γ) c = N-ob η c ⋆⟨ D ⟩ N-ob γ c + N-hom (compWildNatTrans η γ) {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 _ _ _) + + compWildNatIso : WildNatIso _ _ F G → WildNatIso _ _ G H → WildNatIso _ _ F H + trans (compWildNatIso isη isγ) = compWildNatTrans (trans isη) (trans isγ) + inv' (isIs (compWildNatIso isη isγ) c) = inv' (isIs isγ c) ⋆⟨ D ⟩ (inv' (isIs isη c)) + sect (isIs (compWildNatIso 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 (compWildNatIso 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 : WildCat ℓC ℓC'} {D : WildCat ℓD ℓD'} {E : WildCat ℓE ℓE'} + where + comp-WildFunctor : (F : WildFunctor C D) (G : WildFunctor D E) + → WildFunctor C E + F-ob (comp-WildFunctor F G) c = F-ob G (F-ob F c) + F-hom (comp-WildFunctor F G) f = F-hom G (F-hom F f) + F-id (comp-WildFunctor F G) = cong (F-hom G) (F-id F) ∙ F-id G + F-seq (comp-WildFunctor F G) f g = cong (F-hom G) (F-seq F f g) ∙ F-seq G _ _ + + +module _ {C : WildCat ℓC ℓC'} + (F : WildFunctor (C × C) C) where + assocₗ : WildFunctor (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ᵣ : WildFunctor (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 _ _ + +-- Left and right restrictions of functors +module _ + {C : WildCat ℓC ℓC'} + {D : WildCat ℓD ℓD'} + {E : WildCat ℓE ℓE'} + where + restrFunctorₗ : (F : WildFunctor (C × D) E) (c : C . ob) + → WildFunctor 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 : WildFunctor (C × D) E) (d : D . ob) + → WildFunctor 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) + +-- Identity functor +idWildFunctor : {ℓC ℓC' : Level} + (C : WildCat ℓC ℓC') + → WildFunctor C C +WildFunctor.F-ob (idWildFunctor C) c = c +WildFunctor.F-hom (idWildFunctor C) x = x +WildFunctor.F-id (idWildFunctor C) = refl +WildFunctor.F-seq (idWildFunctor C) _ _ = refl + +-- Commutator +commFunctor : {ℓC ℓC' ℓD ℓD' : Level} + {C : WildCat ℓC ℓC'} + {D : WildCat ℓD ℓD'} + → WildFunctor (C × D) (D × C) +WildFunctor.F-ob commFunctor (x , y) = y , x +WildFunctor.F-hom commFunctor (f , g) = g , f +WildFunctor.F-id commFunctor = refl +WildFunctor.F-seq commFunctor _ _ = refl diff --git a/Cubical/WildCat/Instances/Categories.agda b/Cubical/WildCat/Instances/Categories.agda new file mode 100644 index 0000000000..2edd8d9d0f --- /dev/null +++ b/Cubical/WildCat/Instances/Categories.agda @@ -0,0 +1,26 @@ +-- The wild category of (small) categories +{-# OPTIONS --safe #-} + +module Cubical.WildCat.Instances.Categories where + +open import Cubical.Foundations.Prelude + +open import Cubical.Categories.Category.Base +open import Cubical.Categories.Functor.Base +open import Cubical.Categories.Functor.Properties + +open import Cubical.WildCat.Base + +module _ (ℓ ℓ' : Level) where + open WildCat + + CatWildCat : WildCat (ℓ-suc (ℓ-max ℓ ℓ')) (ℓ-max ℓ ℓ') + CatWildCat .ob = Category ℓ ℓ' + CatWildCat .Hom[_,_] = Functor + CatWildCat .id = 𝟙⟨ _ ⟩ + CatWildCat ._⋆_ G H = H ∘F G + CatWildCat .⋆IdL _ = F-lUnit + CatWildCat .⋆IdR _ = F-rUnit + CatWildCat .⋆Assoc _ _ _ = F-assoc + +-- TODO: what is required for Functor C D to be a set? diff --git a/Cubical/WildCat/Instances/Path.agda b/Cubical/WildCat/Instances/Path.agda new file mode 100644 index 0000000000..03db3a1b57 --- /dev/null +++ b/Cubical/WildCat/Instances/Path.agda @@ -0,0 +1,22 @@ +{-# OPTIONS --safe #-} +module Cubical.WildCat.Instances.Path where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.GroupoidLaws + +open import Cubical.WildCat.Base + +private + variable + ℓ : Level + +open WildCat + +PathCat : (A : Type ℓ) → WildCat ℓ ℓ +ob (PathCat A) = A +Hom[_,_] (PathCat A) x y = (x ≡ y) +id (PathCat A) = refl +_⋆_ (PathCat A) = _∙_ +⋆IdL (PathCat A) p = sym (lUnit p) +⋆IdR (PathCat A) p = sym (rUnit p) +⋆Assoc (PathCat A) p q r = sym (assoc p q r) diff --git a/Cubical/WildCat/Instances/Pointed.agda b/Cubical/WildCat/Instances/Pointed.agda new file mode 100644 index 0000000000..a5468651ca --- /dev/null +++ b/Cubical/WildCat/Instances/Pointed.agda @@ -0,0 +1,18 @@ +{-# OPTIONS --safe #-} +module Cubical.WildCat.Instances.Pointed where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Pointed hiding (⋆ ; id) + +open import Cubical.WildCat.Base + +open WildCat + +PointedCat : (ℓ : Level) → WildCat (ℓ-suc ℓ) ℓ +ob (PointedCat ℓ) = Pointed ℓ +Hom[_,_] (PointedCat ℓ) A B = A →∙ B +WildCat.id (PointedCat ℓ) = idfun∙ _ +_⋆_ (PointedCat ℓ) f g = g ∘∙ f +⋆IdL (PointedCat ℓ) = ∘∙-idˡ +⋆IdR (PointedCat ℓ) = ∘∙-idʳ +⋆Assoc (PointedCat ℓ) f g h = sym (∘∙-assoc h g f) diff --git a/Cubical/WildCat/Instances/Types.agda b/Cubical/WildCat/Instances/Types.agda new file mode 100644 index 0000000000..b6024f2da3 --- /dev/null +++ b/Cubical/WildCat/Instances/Types.agda @@ -0,0 +1,19 @@ +{-# OPTIONS --safe #-} +module Cubical.WildCat.Instances.Types where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Pointed hiding (⋆ ; id) +open import Cubical.Foundations.Function using (idfun) renaming (_∘_ to _∘fun_) + +open import Cubical.WildCat.Base + +open WildCat + +TypeCat : (ℓ : Level) → WildCat (ℓ-suc ℓ) ℓ +ob (TypeCat ℓ) = Type ℓ +Hom[_,_] (TypeCat ℓ) A B = A → B +WildCat.id (TypeCat ℓ) = idfun _ +_⋆_ (TypeCat ℓ) f g = g ∘fun f +⋆IdL (TypeCat ℓ) = λ _ → refl +⋆IdR (TypeCat ℓ) = λ _ → refl +⋆Assoc (TypeCat ℓ) f g h = refl diff --git a/Cubical/WildCat/Product.agda b/Cubical/WildCat/Product.agda new file mode 100644 index 0000000000..3201634e0d --- /dev/null +++ b/Cubical/WildCat/Product.agda @@ -0,0 +1,26 @@ +{-# OPTIONS --safe #-} +module Cubical.WildCat.Product where + +open import Cubical.Foundations.Prelude + +open import Cubical.Data.Sigma renaming (_×_ to _×'_) + +open import Cubical.WildCat.Base + +private + variable + ℓ ℓ' : Level + ℓC ℓC' ℓD ℓD' : Level + +open WildCat + +_×_ : (C : WildCat ℓC ℓC') (D : WildCat ℓD ℓD') → WildCat _ _ +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