Code

WIP: quotients#48

Code

Open

marcosh wants to merge 34 commits intomasterstatebox/idris-ct:masterfrom free-andrekstatebox/idris-ct:free-andrekCopy head branch name to clipboard

+730-1

Commits

Commits on Jun 11, 2019

• start defining free monoidal categories

  marcosh

  committed
  2de4945

• definition for free category morphisms

  marcosh

  committed
  ee56056

• Free categories defined.

  

  FabrizioRomanoGenovese

  authored and

  marcosh

  committed
  b472c43

• add license head to free monoidal category

  marcosh

  committed
  184a519

• progress on free monoidal category

  marcosh

  committed
  900199f

• solving free category tensor issue

  marcosh

  committed
  f844bf7

• complete free monoidal category definition

  marcosh

  committed
  6b456a3

• strict symmetric monoidal category (inverse missing)

  marcosh

  committed
  d32bea3

• inverse law for strict symmetric monoidal categories

  marcosh

  committed
  4d5bcef

• progress on FreeMonoidalCategory

  marcosh

  committed
  3a95eab

• complete freeSymmetryCommutativity proof

  marcosh

  committed
  fbabc8d

• complete free strict symmetric monoidal category with mistake

  marcosh

  committed
  0fe4bdf

• complete definition of free strict symmetric monoidal category

  marcosh

  committed
  e2917db

• add license to free monoid file

  marcosh

  committed
  b5f65cd

• remove newlines

  marcosh

  committed
  e1cf9de

• removed unused imports

  marcosh

  committed
  fea7f48

• coherently use generatingMorphisms

  marcosh

  committed
  65477bf

• avoid paradoxes by disabling pattern matching on FreeMorphism

  marcosh

  committed
  65571ec

• start implementing monoidal functor

  marcosh

  committed
  ab21bca

• start defining a fold on free strict symmetric monoidal category

  marcosh

  committed
  4c28710

• Agda experiment constructing free sym mon cat on a cat

  

  fredrikNordvallForsberg

  authored and

  marcosh

  committed
  8d493bc

• remove fred experiment from free-marcosh branch

  marcosh

  committed
  3213b10

• remove definition of monoidal functor from free-marcosh branch

  marcosh

  committed
  7a10a8e

• add namespace to module name

  marcosh

  committed
  1ccb775

• add getters for strict symmetric monoidal category

  marcosh

  committed
  468d379

• start defining monoid instance for strict monoidal category objects

  marcosh

  committed
  15eb353

• progress with free monoidal category fold

  marcosh

  committed
  d696bf6

Commits on Aug 27, 2019

• Add code for generating and working with quotients

  WhatisRT

  committed
  7ff772f

• Remove some unnecessary stuff

  WhatisRT

  committed
  94d4600

• Implemented some of Frederik's suggestions

  WhatisRT

  committed
  b142fa4

Commits on Sep 2, 2019

• Add quotients by arbitrary relations, by forming an equivalence closure

  WhatisRT

  committed
  5a9201e

• Merge branch 'quotients' into free-andrek

  WhatisRT

  committed
  c78b3b1

Commits on Sep 10, 2019

• Add some morphisms for free categories using the new quotients

  WhatisRT

  committed
  8fdbead

Commits on Sep 11, 2019

• fix quotient namespaces

  marcosh

  committed
  3c54b5f