search

ohnosequences / stuff

Useful stuff.
GNU Affero General Public License v3.0
1 stars 0 forks source link

Monoid morphisms; how? #41

Closed eparejatobes closed 6 years ago

eparejatobes commented 7 years ago

Is it a good idea to create a type for monoid morphisms? it would "only" serve as a marker that something is assumed to be a monoid morphism. In some cases we know externally that something is a monoid morphism; on the other hand, library users could then "fix" errors by simply building onesuch.

Sample code:

final
  class MonoidMorphism[MCat <: MonoidalCategory, M <: Monoid.In[MCat], N <: Monoid.In[MCat]](val f: MCat#On#C[M#M, N#M])

  final
  class MonoidsCategory[MCat <: MonoidalCategory](val mcat: MCat) extends Category {

    type Objects =
      Monoid.In[MCat]

    type C[A <: Objects, B <: Objects] =
      MonoidMorphism[MCat, A, B]

    def identity[X <: Objects]: C[X,X] =
      new MonoidMorphism( Category.is(MonoidalCategory.is(mcat).on).identity )

    def composition[X <: Objects, Y <: Objects, Z <: Objects]: C[X,Y] × C[Y,Z] -> C[X,Z] =
      λ((_:C[X,Y]).f) × λ((_:C[Y,Z]).f) >-> Category.is(MonoidalCategory.is(mcat).on).composition >-> λ(new MonoidMorphism(_))
  }
eparejatobes commented 6 years ago

Monoids and related structures will be dealt with elsewhere.