-- Copy Monads as in "Restriction Categories III"

open import Level
open import Categories.Category.Core
open import Categories.Category.Cartesian
open import Categories.Category.BinaryProducts
open import Categories.Monad hiding (id)
open import Categories.Monad.Strong
open import Categories.Monad.Commutative
open import Categories.Category.Cartesian.Monoidal
open import Categories.Category.Cartesian.SymmetricMonoidal
open import Categories.Category.Monoidal.Symmetric using (Symmetric)

import Categories.Monad.Strong.Properties as StrongProps

module Monad.Copy {o ℓ e} {C : Category o ℓ e} (cartesian : Cartesian C) where
  open Category C
  open Cartesian cartesian using (products)
  open BinaryProducts products
  open CartesianMonoidal cartesian using (monoidal)
  open Symmetric (symmetric C cartesian) using (braided)

  Copy : ∀ (CM : CommutativeMonad braided) → Set (o ⊔ e)
  Copy CM = ∀ {X} → (M.μ.η _ ∘ M.F.₁ τ) ∘ σ ∘ Δ {M.F.₀ X} ≈ M.F.₁ Δ
    where
      open CommutativeMonad CM
      open StrongProps.Right.Shorthands rightStrength
      open StrongProps.Left.Shorthands strength

  record CopyMonad : Set (o ⊔ ℓ ⊔ e)
    where
      field
        commutativeMonad : CommutativeMonad braided
        copy : Copy commutativeMonad

      open CommutativeMonad commutativeMonad public
      open StrongProps.Right.Shorthands rightStrength public
      open StrongProps.Left.Shorthands strength public