From 6c7137fef4fe71babad484f85982bc0f44363a1c Mon Sep 17 00:00:00 2001
From: Jordan Barrett <90195985+barrettj12@users.noreply.github.com>
Date: Fri, 26 Nov 2021 18:27:43 +0100
Subject: [PATCH 1/3] Product of categories

---
 Cubical/Categories/Constructions/Product.agda | 64 +++++++++++++++++++
 Cubical/Categories/Functor.agda               |  3 +-
 Cubical/Categories/Functor/Product.agda       | 26 ++++++++
 3 files changed, 92 insertions(+), 1 deletion(-)
 create mode 100644 Cubical/Categories/Constructions/Product.agda
 create mode 100644 Cubical/Categories/Functor/Product.agda

diff --git a/Cubical/Categories/Constructions/Product.agda b/Cubical/Categories/Constructions/Product.agda
new file mode 100644
index 0000000000..a013278ea8
--- /dev/null
+++ b/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
+-}
diff --git a/Cubical/Categories/Functor.agda b/Cubical/Categories/Functor.agda
index f985a8b1b5..8932baee20 100644
--- a/Cubical/Categories/Functor.agda
+++ b/Cubical/Categories/Functor.agda
@@ -3,5 +3,6 @@
 module Cubical.Categories.Functor where
 
 open import Cubical.Categories.Functor.Base public
-open import Cubical.Categories.Functor.Properties public
 open import Cubical.Categories.Functor.Compose public
+open import Cubical.Categories.Functor.Product public
+open import Cubical.Categories.Functor.Properties public
diff --git a/Cubical/Categories/Functor/Product.agda b/Cubical/Categories/Functor/Product.agda
new file mode 100644
index 0000000000..85c2272ee7
--- /dev/null
+++ b/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 _ _)

From 33d9c204d38abb89fba7add44bdc62582da474c5 Mon Sep 17 00:00:00 2001
From: Jordan Barrett <90195985+barrettj12@users.noreply.github.com>
Date: Tue, 14 Dec 2021 18:16:28 +0100
Subject: [PATCH 2/3] Add monoidal & enriched categories

---
 Cubical/Categories/Category/Base.agda     |   3 +
 Cubical/Categories/Monoidal.agda          |   7 ++
 Cubical/Categories/Monoidal/Base.agda     | 121 ++++++++++++++++++++++
 Cubical/Categories/Monoidal/Enriched.agda |  29 ++++++
 4 files changed, 160 insertions(+)
 create mode 100644 Cubical/Categories/Monoidal.agda
 create mode 100644 Cubical/Categories/Monoidal/Base.agda
 create mode 100644 Cubical/Categories/Monoidal/Enriched.agda

diff --git a/Cubical/Categories/Category/Base.agda b/Cubical/Categories/Category/Base.agda
index 8e0f7dc716..36606c14dd 100644
--- a/Cubical/Categories/Category/Base.agda
+++ b/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
diff --git a/Cubical/Categories/Monoidal.agda b/Cubical/Categories/Monoidal.agda
new file mode 100644
index 0000000000..bc2a153a14
--- /dev/null
+++ b/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
diff --git a/Cubical/Categories/Monoidal/Base.agda b/Cubical/Categories/Monoidal/Base.agda
new file mode 100644
index 0000000000..c51e55d312
--- /dev/null
+++ b/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
+        i : 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 →  i ⊗ x ≡ x
+      idr : ∀ x →  x ⊗ i ≡ x
+
+
+  record MonoidalStr : Type (ℓ-max ℓ ℓ') where
+    field
+      tenstr : TensorStr
+
+    open TensorStr tenstr public
+
+    private
+      -- Give some names to things
+      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 ⟩
+      i⊗x = ─⊗─ ∘F (rinj C C i)
+      x⊗i = ─⊗─ ∘F (linj C C i)
+
+    field
+      -- "Axioms" - up to natural isomorphism
+      α : x⊗[y⊗z] ≅ᶜ [x⊗y]⊗z
+      η : i⊗x ≅ᶜ x
+      ρ : x⊗i ≅ᶜ 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[ i ⊗ x , x ]
+    η⟨ x ⟩ = η .trans ⟦ x ⟧
+
+    ρ⟨_⟩ : (x : ob) → Hom[ x ⊗ i , 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 , i , 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 , i ⊗ x ]
+    η⁻¹⟨ x ⟩ = η .nIso (x) .inv
+
+    ρ⁻¹⟨_⟩ : (x : ob) → Hom[ x , x ⊗ i ]
+    ρ⁻¹⟨ 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
diff --git a/Cubical/Categories/Monoidal/Enriched.agda b/Cubical/Categories/Monoidal/Enriched.agda
new file mode 100644
index 0000000000..445cd07dab
--- /dev/null
+++ b/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[ i , 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[ i , Hom[ x , y ] ]

From c6727c0590ee0c26255f42e2b1afd2a5ffa17bb2 Mon Sep 17 00:00:00 2001
From: Jordan Barrett <90195985+barrettj12@users.noreply.github.com>
Date: Fri, 17 Dec 2021 11:06:15 +0100
Subject: [PATCH 3/3] Fix names

---
 Cubical/Categories/Monoidal/Base.agda     | 26 +++++++++++------------
 Cubical/Categories/Monoidal/Enriched.agda |  4 ++--
 2 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/Cubical/Categories/Monoidal/Base.agda b/Cubical/Categories/Monoidal/Base.agda
index c51e55d312..c9f0e7546f 100644
--- a/Cubical/Categories/Monoidal/Base.agda
+++ b/Cubical/Categories/Monoidal/Base.agda
@@ -19,7 +19,7 @@ module _ {ℓ ℓ' : Level} (C : Category ℓ ℓ') where
     record TensorStr : Type (ℓ-max ℓ ℓ') where
       field
         ─⊗─ : Functor (C × C) C
-        i : ob
+        unit : ob
 
       open Functor
 
@@ -41,8 +41,8 @@ module _ {ℓ ℓ' : Level} (C : Category ℓ ℓ') where
     field
       -- Axioms - strict
       assoc : ∀ x y z →  x ⊗ (y ⊗ z) ≡ (x ⊗ y) ⊗ z
-      idl : ∀ x →  i ⊗ x ≡ x
-      idr : ∀ x →  x ⊗ i ≡ x
+      idl : ∀ x →  unit ⊗ x ≡ x
+      idr : ∀ x →  x ⊗ unit ≡ x
 
 
   record MonoidalStr : Type (ℓ-max ℓ ℓ') where
@@ -52,7 +52,7 @@ module _ {ℓ ℓ' : Level} (C : Category ℓ ℓ') where
     open TensorStr tenstr public
 
     private
-      -- Give some names to things
+      -- Private names to make the axioms below look nice
       x⊗[y⊗z] : Functor (C × C × C) C
       x⊗[y⊗z] = ─⊗─ ∘F (𝟙⟨ C ⟩ ×F ─⊗─)
 
@@ -60,14 +60,14 @@ module _ {ℓ ℓ' : Level} (C : Category ℓ ℓ') where
       [x⊗y]⊗z = ─⊗─ ∘F (─⊗─ ×F 𝟙⟨ C ⟩) ∘F (×C-assoc C C C)
 
       x = 𝟙⟨ C ⟩
-      i⊗x = ─⊗─ ∘F (rinj C C i)
-      x⊗i = ─⊗─ ∘F (linj C C i)
+      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
-      η : i⊗x ≅ᶜ x
-      ρ : x⊗i ≅ᶜ x
+      η : 1⊗x ≅ᶜ x
+      ρ : x⊗1 ≅ᶜ x
 
     open NatIso
 
@@ -75,10 +75,10 @@ module _ {ℓ ℓ' : Level} (C : Category ℓ ℓ') where
     α⟨_,_,_⟩ : (x y z : ob) → Hom[ x ⊗ (y ⊗ z) , (x ⊗ y) ⊗ z ]
     α⟨ x , y , z ⟩ = α .trans ⟦ ( x , y , z ) ⟧
 
-    η⟨_⟩ : (x : ob) → Hom[ i ⊗ x , x ]
+    η⟨_⟩ : (x : ob) → Hom[ unit ⊗ x , x ]
     η⟨ x ⟩ = η .trans ⟦ x ⟧
 
-    ρ⟨_⟩ : (x : ob) → Hom[ x ⊗ i , x ]
+    ρ⟨_⟩ : (x : ob) → Hom[ x ⊗ unit , x ]
     ρ⟨ x ⟩ = ρ .trans ⟦ x ⟧
 
     field
@@ -88,7 +88,7 @@ module _ {ℓ ℓ' : Level} (C : Category ℓ ℓ') where
             ≡   α⟨ w , x , y ⊗ z ⟩  ⋆  α⟨ w ⊗ x , y , z ⟩
 
       triangle : ∀ x y →
-        α⟨ x , i , y ⟩  ⋆  ρ⟨ x ⟩ ⊗ₕ id  ≡  id ⊗ₕ η⟨ y ⟩
+        α⟨ x , unit , y ⟩  ⋆  ρ⟨ x ⟩ ⊗ₕ id  ≡  id ⊗ₕ η⟨ y ⟩
 
     open isIso
 
@@ -96,10 +96,10 @@ module _ {ℓ ℓ' : Level} (C : Category ℓ ℓ') where
     α⁻¹⟨_,_,_⟩ : (x y z : ob) → Hom[ (x ⊗ y) ⊗ z , x ⊗ (y ⊗ z) ]
     α⁻¹⟨ x , y , z ⟩ = α .nIso (x , y , z) .inv
 
-    η⁻¹⟨_⟩ : (x : ob) → Hom[ x , i ⊗ x ]
+    η⁻¹⟨_⟩ : (x : ob) → Hom[ x , unit ⊗ x ]
     η⁻¹⟨ x ⟩ = η .nIso (x) .inv
 
-    ρ⁻¹⟨_⟩ : (x : ob) → Hom[ x , x ⊗ i ]
+    ρ⁻¹⟨_⟩ : (x : ob) → Hom[ x , x ⊗ unit ]
     ρ⁻¹⟨ x ⟩ = ρ .nIso (x) .inv
 
 
diff --git a/Cubical/Categories/Monoidal/Enriched.agda b/Cubical/Categories/Monoidal/Enriched.agda
index 445cd07dab..c7ea5d60ad 100644
--- a/Cubical/Categories/Monoidal/Enriched.agda
+++ b/Cubical/Categories/Monoidal/Enriched.agda
@@ -15,7 +15,7 @@ module _ {ℓV ℓV' : Level} (V : MonoidalCategory ℓV ℓV') (ℓE : Level) w
     field
       ob : Type ℓE
       Hom[_,_] : ob → ob → obV
-      id : ∀ {x} → V[ i , Hom[ x , x ] ]
+      id : ∀ {x} → V[ unit , Hom[ x , x ] ]
       seq : ∀ x y z → V[ Hom[ x , y ] ⊗ Hom[ y , z ] , Hom[ x , z ] ]
 
       -- Axioms
@@ -26,4 +26,4 @@ module _ {ℓV ℓV' : Level} (V : MonoidalCategory ℓV ℓV') (ℓE : Level) w
                           ≡  (idV ⊗ₕ (seq y z w))  ⋆V  (seq x y w)
 
 
--- TODO: define underlying category using Hom[ x , y ] := V[ i , Hom[ x , y ] ]
+-- TODO: define underlying category using Hom[ x , y ] := V[ unit , Hom[ x , y ] ]