{-# 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.Monoid.Frobenius {o ℓ e : Level} {C : Category o ℓ e} {M : Monoidal C} (S : Symmetric M) where

open import Categories.Category.Monoidal.Symmetric.Properties S using () renaming (symmetric-Op to Sᵒᵖ)
open import Object.Monoid.Commutative using (IsCommutativeMonoid)

open Category C

record IsSpecialCommutativeFrobeniusMonoid (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
    special : μ ∘ δ ≈ id

record SpecialCommutativeFrobeniusMonoid : Set (o ⊔ ℓ ⊔ e) where

  field
    Carrier : Obj
    isSpecialCommutativeFrobeniusMonoid : IsSpecialCommutativeFrobeniusMonoid Carrier

  open IsSpecialCommutativeFrobeniusMonoid isSpecialCommutativeFrobeniusMonoid public