1 files changed, 102 insertions, 0 deletions
diff --git a/Object/Bimonoid.agda b/Object/Bimonoid.agda
new file mode 100644
index 0000000..c53e122
--- /dev/null
+++ b/Object/Bimonoid.agda
@@ -0,0 +1,102 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Level using (Level; _⊔_)
+
+module Object.Bimonoid {o ℓ e : Level} {C : Category o ℓ e} {M : Monoidal C} (S : Symmetric M) where
+
+import Categories.Category.Monoidal.Interchange.Braided as Interchange
+
+open import Categories.Category.Monoidal.Properties M using () renaming (monoidal-Op to Mᵒᵖ)
+open import Categories.Category.Monoidal.Symmetric.Properties S using () renaming (symmetric-Op to Sᵒᵖ)
+open import Categories.Category.Monoidal.Utilities M using (module Shorthands)
+open import Categories.Object.Monoid using (IsMonoid)
+open import Object.Monoid.Commutative using (IsCommutativeMonoid)
+
+open Category C
+open Symmetric S
+
+open Interchange braided using (module swapInner)
+open Shorthands using (λ⇒; λ⇐)
+
+open swapInner renaming (from to i⇒)
+
+record IsBimonoid (A : Obj) : Set (ℓ ⊔ e) where
+
+  field
+    monoid : IsMonoid M A
+    comonoid : IsMonoid Mᵒᵖ A
+
+  open IsMonoid monoid
+    using (μ; η)
+    renaming (assoc to μ-assoc; identityˡ to μ-η-identityˡ; identityʳ to μ-η-identityʳ)
+    public
+
+  open IsMonoid comonoid
+    using ()
+    renaming (μ to δ; η to ϵ; assoc to δ-assoc; identityˡ to δ-ϵ-identityˡ; identityʳ to δ-ϵ-identityʳ)
+    public
+
+  field
+    μ-δ-compat : δ ∘ μ ≈ μ ⊗₁ μ ∘ i⇒ ∘ δ ⊗₁ δ
+    μ-ϵ-compat : ϵ ∘ μ ≈ λ⇒ ∘ ϵ ⊗₁ ϵ
+    δ-η-compat : δ ∘ η ≈ η ⊗₁ η ∘ λ⇐
+    extra : ϵ ∘ η ≈ id
+
+record Bimonoid : Set (o ⊔ ℓ ⊔ e) where
+
+  field
+    Carrier : Obj
+    isBimonoid : IsBimonoid Carrier
+
+  open IsBimonoid isBimonoid public
+
+record IsBicommutativeBimonoid (A : Obj) : Set (ℓ ⊔ e) where
+
+  field
+    commutativeMonoid : IsCommutativeMonoid S A
+    cocommutativeComonoid : IsCommutativeMonoid Sᵒᵖ A
+
+  open IsCommutativeMonoid commutativeMonoid
+    using (μ; η; commutative)
+    renaming (assoc to μ-assoc; identityˡ to μ-η-identityˡ; identityʳ to μ-η-identityʳ)
+    public
+
+  open IsCommutativeMonoid cocommutativeComonoid
+    using ()
+    renaming (μ to δ; η to ϵ; assoc to δ-assoc; identityˡ to δ-ϵ-identityˡ; identityʳ to δ-ϵ-identityʳ; commutative to cocommutative)
+    public
+
+  field
+    μ-η-compat : δ ∘ μ ≈ μ ⊗₁ μ ∘ i⇒ ∘ δ ⊗₁ δ
+    μ-ϵ-compat : ϵ ∘ μ ≈ λ⇒ ∘ ϵ ⊗₁ ϵ
+    δ-η-compat : δ ∘ η ≈ η ⊗₁ η ∘ λ⇐
+    extra : ϵ ∘ η ≈ id
+
+record BicommutativeBimonoid : Set (o ⊔ ℓ ⊔ e) where
+
+  field
+    Carrier : Obj
+    isBicommutativeBimonoid : IsBicommutativeBimonoid Carrier
+
+  open IsBicommutativeBimonoid isBicommutativeBimonoid public
+
+record IsSpecialBicommutativeBimonoid (A : Obj) : Set (ℓ ⊔ e) where
+
+  field
+    bimonoid : IsBicommutativeBimonoid A
+
+  open IsBicommutativeBimonoid bimonoid public
+
+  field
+    special : μ ∘ δ ≈ id
+
+record SpecialBicommutativeBimonoid : Set (o ⊔ ℓ ⊔ e) where
+
+  field
+    Carrier : Obj
+    isSpecialBicommutativeBimonoid : IsSpecialBicommutativeBimonoid Carrier
+
+  open IsSpecialBicommutativeBimonoid isSpecialBicommutativeBimonoid public