free strict symmetric monoidal category#21

Open

marcosh wants to merge 27 commits intomasterfrom

free-marcosh

Commits on Jun 11, 2019

start defining free monoidal categories
marcosh
committed
definition for free category morphisms
marcosh
committed
Free categories defined.

FabrizioRomanoGenovese
authored and
marcosh
committed
add license head to free monoidal category
marcosh
committed
progress on free monoidal category
marcosh
committed
solving free category tensor issue
marcosh
committed
complete free monoidal category definition
marcosh
committed
strict symmetric monoidal category (inverse missing)
marcosh
committed
inverse law for strict symmetric monoidal categories
marcosh
committed
progress on FreeMonoidalCategory
marcosh
committed
complete freeSymmetryCommutativity proof
marcosh
committed
complete free strict symmetric monoidal category with mistake
marcosh
committed
complete definition of free strict symmetric monoidal category
marcosh
committed
add license to free monoid file
marcosh
committed
remove newlines
marcosh
committed
removed unused imports
marcosh
committed
coherently use `generatingMorphisms`
marcosh
committed
avoid paradoxes by disabling pattern matching on FreeMorphism
marcosh
committed
start implementing monoidal functor
marcosh
committed
start defining a fold on free strict symmetric monoidal category
marcosh
committed
Agda experiment constructing free sym mon cat on a cat

fredrikNordvallForsberg
authored and
marcosh
committed
remove fred experiment from free-marcosh branch
marcosh
committed
remove definition of monoidal functor from free-marcosh branch
marcosh
committed
add namespace to module name
marcosh
committed
add getters for strict symmetric monoidal category
marcosh
committed
start defining monoid instance for strict monoidal category objects
marcosh
committed
progress with free monoidal category fold
marcosh
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

free strict symmetric monoidal category#21

free strict symmetric monoidal category#21
marcosh wants to merge 27 commits intomasterfrom
free-marcosh

Commits on Jun 11, 2019

start defining free monoidal categories

definition for free category morphisms

Free categories defined.

add license head to free monoidal category

progress on free monoidal category

solving free category tensor issue

complete free monoidal category definition

strict symmetric monoidal category (inverse missing)

inverse law for strict symmetric monoidal categories

progress on FreeMonoidalCategory

complete freeSymmetryCommutativity proof

complete free strict symmetric monoidal category with mistake

complete definition of free strict symmetric monoidal category

add license to free monoid file

remove newlines

removed unused imports

coherently use `generatingMorphisms`

avoid paradoxes by disabling pattern matching on FreeMorphism

start implementing monoidal functor

start defining a fold on free strict symmetric monoidal category

Agda experiment constructing free sym mon cat on a cat

remove fred experiment from free-marcosh branch

remove definition of monoidal functor from free-marcosh branch

add namespace to module name

add getters for strict symmetric monoidal category

start defining monoid instance for strict monoidal category objects

progress with free monoidal category fold