Add monoidal preorders to monoids functor

2 files changed, 161 insertions, 0 deletions

diff --git a/Functor/Cartesian/Instance/InducedSetoid.agda b/Functor/Cartesian/Instance/InducedSetoid.agda
new file mode 100644
index 0000000..fa46290
--- /dev/null
+++ b/Functor/Cartesian/Instance/InducedSetoid.agda
@@ -0,0 +1,54 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Cartesian.Instance.InducedSetoid where
+
+-- The induced setoid functor is cartesian
+
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-CartesianCategory)
+open import Categories.Functor.Cartesian using (CartesianF)
+open import Categories.Object.Product using (IsProduct)
+open import Category.Cartesian.Instance.Preorders.Primitive using (Preorders-CC)
+open import Data.Product using (<_,_>; _,_)
+open import Function using (Func)
+open import Functor.Free.Instance.InducedSetoid using () renaming (InducedSetoid to IS)
+open import Level using (Level)
+open import Preorder.Primitive using (Preorder; module Isomorphism)
+
+module _ {c ℓ : Level} where
+
+  private
+    module Preorders-CC = CartesianCategory (Preorders-CC c ℓ)
+    module BP = BinaryProducts (Preorders-CC.products)
+
+    IS-resp-×
+        : {A B : Preorder c ℓ}
+        → IsProduct (Setoids c ℓ) (IS.₁ {B = A} (BP.π₁ {B = B})) (IS.₁ BP.π₂)
+    IS-resp-× {A} {B} = record
+        { ⟨_,_⟩ = λ {S} S⟶ₛIS₀A S⟶ₛIS₀B → let open Func in record
+            { to = < to S⟶ₛIS₀A , to S⟶ₛIS₀B >
+            ; cong = λ x≈y → let open Isomorphism._≅_ in record
+                { from = from (cong S⟶ₛIS₀A x≈y) , from (cong S⟶ₛIS₀B x≈y)
+                ; to = to (cong S⟶ₛIS₀A x≈y) , to (cong S⟶ₛIS₀B x≈y)
+                }
+            }
+        ; project₁ = Isomorphism.≅.refl A
+        ; project₂ = Isomorphism.≅.refl B
+        ; unique = λ {S} {h} {i} {j} π₁∙h≈i π₂∙h≈j {x} → let open Isomorphism._≅_ in record
+            { from = to (π₁∙h≈i {x}) , to (π₂∙h≈j {x})
+            ; to = from (π₁∙h≈i {x}) , from (π₂∙h≈j {x})
+            }
+        }
+
+  InducedSetoid : CartesianF (Preorders-CC c ℓ) (Setoids-CartesianCategory c ℓ)
+  InducedSetoid = record
+      { F = IS
+      ; isCartesian = record
+          { F-resp-⊤ = _
+          ; F-resp-× = IS-resp-×
+          }
+      }
+
+  module InducedSetoid = CartesianF InducedSetoid
diff --git a/Functor/Free/Instance/InducedMonoid.agda b/Functor/Free/Instance/InducedMonoid.agda
new file mode 100644
index 0000000..20cc6e7
--- /dev/null
+++ b/Functor/Free/Instance/InducedMonoid.agda
@@ -0,0 +1,107 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Functor.Free.Instance.InducedMonoid {c ℓ : Level} where
+
+-- The induced monoid of a monoidal preorder
+
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′)
+open import Categories.Object.Monoid Setoids-×.monoidal using (Monoid; Monoid⇒)
+open import Categories.Category.Construction.Monoids Setoids-×.monoidal using (Monoids)
+open import Categories.Functor using (Functor)
+open import Category.Instance.Preorder.Primitive.Monoidals.Strong using (Monoidals)
+open import Category.Cartesian.Instance.Preorders.Primitive using (Preorders-CC; ⊤ₚ)
+open import Preorder.Primitive using (Preorder)
+open import Preorder.Primitive.Monoidal using (MonoidalPreorder; _×ₚ_)
+open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (MonoidalMonotone)
+open import Preorder.Primitive using (module Isomorphism)
+open import Data.Product using (_,_)
+open import Functor.Cartesian.Instance.InducedSetoid using () renaming (module InducedSetoid to IS)
+open import Function using (Func; _⟨$⟩_)
+open import Function.Construct.Setoid using (_∙_)
+open import Data.Setoid.Unit using (⊤ₛ)
+open import Data.Setoid using (∣_∣)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Relation.Binary using (Setoid)
+
+open Setoids-× using (_⊗₀_; _⊗₁_; module unitorˡ; module unitorʳ; module associator; _≈_)
+
+module _ (P : MonoidalPreorder c ℓ) where
+
+  open MonoidalPreorder P
+  open Isomorphism U using (module ≅; _≅_)
+
+  M : Setoid c ℓ
+  M = IS.₀ U
+
+  opaque
+    unfolding ×-monoidal′
+    μ : Func (M ⊗₀ M) M
+    μ = IS.₁ tensor ∙ IS.×-iso.to U U
+
+  η : Func Setoids-×.unit M
+  η = Const Setoids-×.unit M unit
+
+  opaque
+    unfolding μ
+    assoc : μ ∙ μ ⊗₁ Id M ≈ μ ∙ Id M ⊗₁ μ ∙ associator.from
+    assoc {(x , y) , z} = associative x y z
+
+    identityˡ : unitorˡ.from ≈ μ ∙ η ⊗₁ Id M
+    identityˡ {_ , x} = ≅.sym (unitaryˡ x)
+
+    identityʳ : unitorʳ.from ≈ μ ∙ Id M ⊗₁ η
+    identityʳ {x , _} = ≅.sym (unitaryʳ x)
+
+  ≅-monoid : Monoid
+  ≅-monoid = record
+      { Carrier = M
+      ; isMonoid = record
+          { μ = μ
+          ; η = Const Setoids-×.unit M unit
+          ; assoc = assoc
+          ; identityˡ = identityˡ
+          ; identityʳ = identityʳ
+          }
+      }
+
+module _ {A B : MonoidalPreorder c ℓ} (f : MonoidalMonotone A B) where
+
+  private
+    module A = MonoidalPreorder A
+    module B = MonoidalPreorder B
+
+  open Isomorphism B.U using (_≅_; module ≅)
+  open MonoidalMonotone f
+
+  opaque
+    unfolding μ
+    preserves-μ
+        : {x : ∣ IS.₀ A.U ⊗₀ IS.₀ A.U ∣}
+        → map (μ A ⟨$⟩ x)
+        ≅ μ B ⟨$⟩ (IS.₁ F ⊗₁ IS.₁ F ⟨$⟩ x)
+    preserves-μ {x , y} = ≅.sym (⊗-homo x y)
+
+  monoid⇒ : Monoid⇒ (≅-monoid A) (≅-monoid B)
+  monoid⇒ = record
+      { arr = IS.₁ F
+      ; preserves-μ = preserves-μ
+      ; preserves-η = ≅.sym ε
+      }
+
+InducedMonoid : Functor (Monoidals c ℓ) Monoids
+InducedMonoid = record
+    { F₀ = ≅-monoid
+    ; F₁ = monoid⇒
+    ; identity = λ {A} {x} → ≅.refl (U A)
+    ; homomorphism = λ {Z = Z} → ≅.refl (U Z)
+    ; F-resp-≈ = λ f≃g {x} → f≃g x
+    }
+  where
+    open MonoidalPreorder using (U)
+    open Isomorphism using (module ≅)
+
+module InducedMonoid = Functor InducedMonoid