Add monoidal cats to monoidal preorders functor

2 files changed, 161 insertions, 0 deletions

diff --git a/Category/Instance/MonoidalPreorders/Primitive.agda b/Category/Instance/MonoidalPreorders/Primitive.agda
new file mode 100644
index 0000000..d00e17a
--- /dev/null
+++ b/Category/Instance/MonoidalPreorders/Primitive.agda
@@ -0,0 +1,86 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Instance.MonoidalPreorders.Primitive where
+
+import Preorder.Primitive.MonotoneMap as MonotoneMap using (_≃_; module ≃)
+
+open import Categories.Category using (Category)
+open import Categories.Category.Helper using (categoryHelper)
+open import Category.Instance.Preorders.Primitive using (Preorders)
+open import Level using (Level; suc; _⊔_)
+open import Preorder.Primitive.Monoidal using (MonoidalPreorder; MonoidalMonotone)
+open import Relation.Binary using (IsEquivalence)
+
+module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {A : MonoidalPreorder c₁ ℓ₁} {B : MonoidalPreorder c₂ ℓ₂} where
+
+  -- Pointwise equality of monoidal monotone maps
+
+  open MonoidalMonotone using (F)
+
+  _≃_ : (f g : MonoidalMonotone A B) → Set (c₁ ⊔ ℓ₂)
+  f ≃ g = F f MonotoneMap.≃ F g
+
+  infix 4 _≃_
+
+  ≃-isEquivalence : IsEquivalence _≃_
+  ≃-isEquivalence = let open MonotoneMap.≃ in record
+      { refl = λ {x} → refl {x = F x}
+      ; sym = λ {f g} → sym {x = F f} {y = F g}
+      ; trans = λ {f g h} → trans {i = F f} {j = F g} {k = F h}
+      }
+
+  module ≃ = IsEquivalence ≃-isEquivalence
+
+private
+
+  identity : {c ℓ : Level} (A : MonoidalPreorder c ℓ) → MonoidalMonotone A A
+  identity A = let open MonoidalPreorder A in record
+      { F = Category.id (Preorders _ _)
+      ; ε = refl
+      ; ⊗-homo = λ p₁ p₂ → refl {p₁ ⊗ p₂}
+      }
+
+  compose
+      : {c ℓ : Level}
+        {P Q R : MonoidalPreorder c ℓ}
+      → MonoidalMonotone Q R
+      → MonoidalMonotone P Q
+      → MonoidalMonotone P R
+  compose {R = R} G F = record
+      { F = let open Category (Preorders _ _) in G.F ∘ F.F
+      ; ε = trans G.ε (G.mono F.ε)
+      ; ⊗-homo = λ p₁ p₂ → trans (G.⊗-homo (F.map p₁) (F.map p₂)) (G.mono (F.⊗-homo p₁ p₂))
+      }
+    where
+      module F = MonoidalMonotone F
+      module G = MonoidalMonotone G
+      open MonoidalPreorder R
+
+  compose-resp-≃
+      : {c ℓ : Level}
+        {A B C : MonoidalPreorder c ℓ}
+        {f h : MonoidalMonotone B C}
+        {g i : MonoidalMonotone A B}
+      → f ≃ h
+      → g ≃ i
+      → compose f g ≃ compose h i
+  compose-resp-≃ {C = C} {f = f} {g} {h} {i} = ∘-resp-≈ {f = F f} {F g} {F h} {F i}
+    where
+      open Category (Preorders _ _)
+      open MonoidalMonotone using (F)
+
+MonoidalPreorders : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
+MonoidalPreorders c ℓ = categoryHelper record
+    { Obj = MonoidalPreorder c ℓ
+    ; _⇒_ = MonoidalMonotone
+    ; _≈_ = _≃_
+    ; id  = λ {A} → identity A
+    ; _∘_ = compose
+    ; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f}
+    ; identityˡ = λ {f = f} → ≃.refl {x = f}
+    ; identityʳ = λ {f = f} → ≃.refl {x = f}
+    ; equiv = ≃-isEquivalence
+    ; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i}
+    }
+  where
+    open MonoidalMonotone using (F)
diff --git a/Functor/Free/Instance/MonoidalPreorder.agda b/Functor/Free/Instance/MonoidalPreorder.agda
new file mode 100644
index 0000000..ca03786
--- /dev/null
+++ b/Functor/Free/Instance/MonoidalPreorder.agda
@@ -0,0 +1,75 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Free.Instance.MonoidalPreorder where
+
+import Categories.Category.Monoidal.Utilities as ⊗-Util
+
+open import Categories.Category using (Category)
+open import Categories.Category.Instance.Monoidals using (Monoidals)
+open import Categories.Category.Monoidal using (MonoidalCategory)
+open import Categories.Functor using (Functor)
+open import Categories.Functor.Monoidal using (MonoidalFunctor)
+open import Categories.Functor.Monoidal.Properties using (∘-Monoidal)
+open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal using (module Lax)
+open import Category.Instance.MonoidalPreorders.Primitive using (MonoidalPreorders; _≃_; module ≃)
+open import Data.Product using (_,_)
+open import Level using (Level)
+open import Preorder.Primitive.Monoidal using (MonoidalPreorder; MonoidalMonotone)
+
+open Lax using (MonoidalNaturalIsomorphism)
+ 
+-- The free monoidal preorder of a monoidal category
+
+import Functor.Free.Instance.Preorder as Preorder
+
+module _ {o ℓ e : Level} where
+
+  monoidalPreorder : MonoidalCategory o ℓ e → MonoidalPreorder o ℓ
+  monoidalPreorder C = record
+      { U = Preorder.Free.₀ U
+      ; monoidal = record
+          { unit = unit
+          ; tensor = Preorder.Free.₁ ⊗
+          ; unitaryˡ = Preorder.Free.F-resp-≈ unitorˡ-naturalIsomorphism
+          ; unitaryʳ = Preorder.Free.F-resp-≈ unitorʳ-naturalIsomorphism
+          ; associative = λ x y z → record
+              { from = associator.from {x} {y} {z}
+              ; to = associator.to {x} {y} {z}
+              }
+          }
+      }
+    where
+      open MonoidalCategory C
+      open ⊗-Util monoidal
+
+  module _ {A B : MonoidalCategory o ℓ e} where
+
+    monoidalMonotone : MonoidalFunctor A B → MonoidalMonotone (monoidalPreorder A) (monoidalPreorder B)
+    monoidalMonotone F = record
+        { F = Preorder.Free.₁ F.F
+        ; ε = F.ε
+        ; ⊗-homo = λ p₁ p₂ → F.⊗-homo.η (p₁ , p₂)
+        }
+      where
+        module F = MonoidalFunctor F
+
+    open MonoidalNaturalIsomorphism using (U)
+
+    pointwiseIsomorphism
+        : {F G : MonoidalFunctor A B}
+        → MonoidalNaturalIsomorphism F G
+        → monoidalMonotone F ≃ monoidalMonotone G
+    pointwiseIsomorphism F≃G = Preorder.Free.F-resp-≈ (U F≃G)
+
+Free : {o ℓ e : Level} → Functor (Monoidals o ℓ e) (MonoidalPreorders o ℓ)
+Free = record
+    { F₀ = monoidalPreorder
+    ; F₁ = monoidalMonotone
+    ; identity = λ {A} → ≃.refl {A = monoidalPreorder A} {x = id}
+    ; homomorphism = λ {f = f} {h} → ≃.refl {x = monoidalMonotone (∘-Monoidal h f)}
+    ; F-resp-≈ = pointwiseIsomorphism
+    }
+  where
+    open Category (MonoidalPreorders _ _) using (id)
+
+module Free {o ℓ e} = Functor (Free {o} {ℓ} {e})