Add monoidal & enriched categories (#665)

* Product of categories

* Add monoidal & enriched categories

* Fix names

Cubical/Categories/Category/Base.agda

@@ -27,6 +27,9 @@ record Category ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
   _∘_ : ∀ {x y z} (g : Hom[ y , z ]) (f : Hom[ x , y ]) → Hom[ x , z ]
   g ∘ f = f ⋆ g
 
+  infixr 9 _⋆_
+  infixr 9 _∘_
+
 open Category
 
 -- Helpful syntax/notation

Cubical/Categories/Constructions/Product.agda

@@ -0,0 +1,64 @@
+-- Product of two categories
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Constructions.Product where
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor.Base
+open import Cubical.Data.Sigma renaming (_×_ to _×'_)
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Prelude
+
+private
+  variable
+    ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level
+
+
+open Category
+
+_×_ : (C : Category ℓC ℓC') → (D : Category ℓD ℓD')
+    → Category (ℓ-max ℓC ℓD) (ℓ-max ℓC' ℓD')
+
+(C × D) .ob = (ob C) ×' (ob D)
+(C × D) .Hom[_,_] (c , d) (c' , d') = (C [ c , c' ]) ×' (D [ d , d' ])
+(C × D) .id = (id C , id D)
+(C × D) ._⋆_ _ _ = (_ ⋆⟨ C ⟩ _ , _ ⋆⟨ D ⟩ _)
+(C × D) .⋆IdL _ = ≡-× (⋆IdL C _) (⋆IdL D _)
+(C × D) .⋆IdR _ = ≡-× (⋆IdR C _) (⋆IdR D _)
+(C × D) .⋆Assoc _ _ _ = ≡-× (⋆Assoc C _ _ _) (⋆Assoc D _ _ _)
+(C × D) .isSetHom = isSet× (isSetHom C) (isSetHom D)
+
+infixr 5 _×_
+
+
+-- Some useful functors
+module _ (C : Category ℓC ℓC')
+         (D : Category ℓD ℓD') where
+  open Functor
+
+  module _ (E : Category ℓE ℓE') where
+    -- Associativity of product
+    ×C-assoc : Functor (C × (D × E)) ((C × D) × E)
+    ×C-assoc .F-ob (c , (d , e)) = ((c , d), e)
+    ×C-assoc .F-hom (f , (g , h)) = ((f , g), h)
+    ×C-assoc .F-id = refl
+    ×C-assoc .F-seq _ _ = refl
+
+  -- Left/right injections into product
+  linj : (d : ob D) → Functor C (C × D)
+  linj d .F-ob c = (c , d)
+  linj d .F-hom f = (f , id D)
+  linj d .F-id = refl
+  linj d .F-seq f g = ≡-× refl (sym (⋆IdL D _))
+
+  rinj : (c : ob C) → Functor D (C × D)
+  rinj c .F-ob d = (c , d)
+  rinj c .F-hom f = (id C , f)
+  rinj c .F-id = refl
+  rinj c .F-seq f g = ≡-× (sym (⋆IdL C _)) refl
+
+{-
+  TODO:
+    - define inverse to `assoc`, prove isomorphism
+    - prove product is commutative up to isomorphism
+-}

Cubical/Categories/Functor/Product.agda

@@ -0,0 +1,26 @@
+-- Product of two functors
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Functor.Product where
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Constructions.Product
+open import Cubical.Categories.Functor.Base
+open import Cubical.Data.Sigma.Properties
+open import Cubical.Foundations.Prelude
+
+private
+  variable
+    ℓA ℓA' ℓB ℓB' ℓC ℓC' ℓD ℓD' : Level
+    A : Category ℓA ℓA'
+    B : Category ℓB ℓB'
+    C : Category ℓC ℓC'
+    D : Category ℓD ℓD'
+
+open Functor
+
+_×F_ : Functor A C → Functor B D → Functor (A × B) (C × D)
+(G ×F H) .F-ob (a , b) = (G ⟅ a ⟆ , H ⟅ b ⟆)
+(G ×F H) .F-hom (g , h) = (G ⟪ g ⟫ , H ⟪ h ⟫)
+(G ×F H) .F-id = ≡-× (G .F-id) (H .F-id)
+(G ×F H) .F-seq _ _ = ≡-× (G .F-seq _ _) (H .F-seq _ _)

Cubical/Categories/Monoidal.agda

@@ -0,0 +1,7 @@
+-- Monoidal categories
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Monoidal where
+
+open import Cubical.Categories.Monoidal.Base public
+open import Cubical.Categories.Monoidal.Enriched public

Cubical/Categories/Monoidal/Base.agda

@@ -0,0 +1,121 @@
+-- Monoidal categories
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Monoidal.Base where
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Constructions.Product
+open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.Functor.Product
+open import Cubical.Categories.Morphism
+open import Cubical.Categories.NaturalTransformation.Base
+open import Cubical.Foundations.Prelude
+
+
+module _ {ℓ ℓ' : Level} (C : Category ℓ ℓ') where
+  open Category C
+
+  private
+    record TensorStr : Type (ℓ-max ℓ ℓ') where
+      field
+        ─⊗─ : Functor (C × C) C
+        unit : ob
+
+      open Functor
+
+      -- Useful tensor product notation
+      _⊗_ : ob → ob → ob
+      x ⊗ y = ─⊗─ .F-ob (x , y)
+
+      _⊗ₕ_ : ∀ {x y z w} → Hom[ x , y ] → Hom[ z , w ]
+           → Hom[ x ⊗ z , y ⊗ w ]
+      f ⊗ₕ g = ─⊗─ .F-hom (f , g)
+
+
+  record StrictMonStr : Type (ℓ-max ℓ ℓ') where
+    field
+      tenstr : TensorStr
+
+    open TensorStr tenstr public
+
+    field
+      -- Axioms - strict
+      assoc : ∀ x y z →  x ⊗ (y ⊗ z) ≡ (x ⊗ y) ⊗ z
+      idl : ∀ x →  unit ⊗ x ≡ x
+      idr : ∀ x →  x ⊗ unit ≡ x
+
+
+  record MonoidalStr : Type (ℓ-max ℓ ℓ') where
+    field
+      tenstr : TensorStr
+
+    open TensorStr tenstr public
+
+    private
+      -- Private names to make the axioms below look nice
+      x⊗[y⊗z] : Functor (C × C × C) C
+      x⊗[y⊗z] = ─⊗─ ∘F (𝟙⟨ C ⟩ ×F ─⊗─)
+
+      [x⊗y]⊗z : Functor (C × C × C) C
+      [x⊗y]⊗z = ─⊗─ ∘F (─⊗─ ×F 𝟙⟨ C ⟩) ∘F (×C-assoc C C C)
+
+      x = 𝟙⟨ C ⟩
+      1⊗x = ─⊗─ ∘F (rinj C C unit)
+      x⊗1 = ─⊗─ ∘F (linj C C unit)
+
+    field
+      -- "Axioms" - up to natural isomorphism
+      α : x⊗[y⊗z] ≅ᶜ [x⊗y]⊗z
+      η : 1⊗x ≅ᶜ x
+      ρ : x⊗1 ≅ᶜ x
+
+    open NatIso
+
+    -- More nice notations
+    α⟨_,_,_⟩ : (x y z : ob) → Hom[ x ⊗ (y ⊗ z) , (x ⊗ y) ⊗ z ]
+    α⟨ x , y , z ⟩ = α .trans ⟦ ( x , y , z ) ⟧
+
+    η⟨_⟩ : (x : ob) → Hom[ unit ⊗ x , x ]
+    η⟨ x ⟩ = η .trans ⟦ x ⟧
+
+    ρ⟨_⟩ : (x : ob) → Hom[ x ⊗ unit , x ]
+    ρ⟨ x ⟩ = ρ .trans ⟦ x ⟧
+
+    field
+      -- Coherence conditions
+      pentagon : ∀ w x y z →
+        id ⊗ₕ α⟨ x , y , z ⟩  ⋆  α⟨ w , x ⊗ y , z ⟩  ⋆  α⟨ w , x , y ⟩ ⊗ₕ id
+            ≡   α⟨ w , x , y ⊗ z ⟩  ⋆  α⟨ w ⊗ x , y , z ⟩
+
+      triangle : ∀ x y →
+        α⟨ x , unit , y ⟩  ⋆  ρ⟨ x ⟩ ⊗ₕ id  ≡  id ⊗ₕ η⟨ y ⟩
+
+    open isIso
+
+    -- Inverses of α, η, ρ for convenience
+    α⁻¹⟨_,_,_⟩ : (x y z : ob) → Hom[ (x ⊗ y) ⊗ z , x ⊗ (y ⊗ z) ]
+    α⁻¹⟨ x , y , z ⟩ = α .nIso (x , y , z) .inv
+
+    η⁻¹⟨_⟩ : (x : ob) → Hom[ x , unit ⊗ x ]
+    η⁻¹⟨ x ⟩ = η .nIso (x) .inv
+
+    ρ⁻¹⟨_⟩ : (x : ob) → Hom[ x , x ⊗ unit ]
+    ρ⁻¹⟨ x ⟩ = ρ .nIso (x) .inv
+
+
+record StrictMonCategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
+  field
+    C : Category ℓ ℓ'
+    sms : StrictMonStr C
+
+  open Category C public
+  open StrictMonStr sms public
+
+
+record MonoidalCategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
+  field
+    C : Category ℓ ℓ'
+    monstr : MonoidalStr C
+
+  open Category C public
+  open MonoidalStr monstr public

Cubical/Categories/Monoidal/Enriched.agda

@@ -0,0 +1,29 @@
+-- Enriched categories
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Monoidal.Enriched where
+
+open import Cubical.Categories.Monoidal.Base
+open import Cubical.Foundations.Prelude
+
+module _ {ℓV ℓV' : Level} (V : MonoidalCategory ℓV ℓV') (ℓE : Level) where
+
+  open MonoidalCategory V
+    renaming (ob to obV; Hom[_,_] to V[_,_]; id to idV; _⋆_ to _⋆V_)
+
+  record EnrichedCategory : Type (ℓ-max (ℓ-max ℓV ℓV') (ℓ-suc ℓE)) where
+    field
+      ob : Type ℓE
+      Hom[_,_] : ob → ob → obV
+      id : ∀ {x} → V[ unit , Hom[ x , x ] ]
+      seq : ∀ x y z → V[ Hom[ x , y ] ⊗ Hom[ y , z ] , Hom[ x , z ] ]
+
+      -- Axioms
+      ⋆IdL : ∀ x y →   η⟨ _ ⟩  ≡  (id {x} ⊗ₕ idV)  ⋆V  (seq x x y)
+      ⋆IdR : ∀ x y →   ρ⟨ _ ⟩  ≡  (idV ⊗ₕ id {y})  ⋆V  (seq x y y)
+      ⋆Assoc : ∀ x y z w →
+          α⟨ _ , _ , _ ⟩  ⋆V  ((seq x y z) ⊗ₕ idV)  ⋆V  (seq x z w)
+                          ≡  (idV ⊗ₕ (seq y z w))  ⋆V  (seq x y w)
+
+
+-- TODO: define underlying category using Hom[ x , y ] := V[ unit , Hom[ x , y ] ]