{-# 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