Code

[WIP] Preadditive Categories#249

Code

Draft

TOTBWF wants to merge 22 commits intoagda:masteragda/agda-categories:masterfrom TOTBWF:abelian-categoriesTOTBWF/agda-categories:abelian-categoriesCopy head branch name to clipboard

+2,128

Commits

Commits on Feb 22, 2021

• Prove some helpful facts about kernels/zero morphisms

  TOTBWF

  committed
  4cd6012

  Copy full SHA for 4cd6012

• Define Preadditive Categories

  TOTBWF

  committed
  127fc10

  Copy full SHA for 127fc10

• Add a few misc reasoning combinators

  TOTBWF

  committed
  6f427f6

  Copy full SHA for 6f427f6

• Tweak some of the preadditive proof

  TOTBWF

  committed
  7c09b75

  Copy full SHA for 7c09b75

• Define Biproducts

  TOTBWF

  committed
  d8ee5b4

  Copy full SHA for d8ee5b4

• Show that biproducts a-la Maclane coincide with ours

  TOTBWF

  committed
  74fc173

  Copy full SHA for 74fc173

• Add a quick helper lemma to coproducts

  TOTBWF

  committed
  69be86e

  Copy full SHA for 69be86e

• Prove some stuff about biproducts + (co)products

  TOTBWF

  committed
  86de9ef

  Copy full SHA for 86de9ef

• More Preadditive Properties

  TOTBWF

  committed
  ad98503

  Copy full SHA for ad98503

Commits on Mar 1, 2021

• Prove some helpful facts about kernels/zero morphisms

  TOTBWF

  committed
  03b9c4f

  Copy full SHA for 03b9c4f

• Define Preadditive Categories

  TOTBWF

  committed
  2286754

  Copy full SHA for 2286754

• Tweak some of the preadditive proof

  TOTBWF

  committed
  15eb188

  Copy full SHA for 15eb188

• Show that biproducts a-la Maclane coincide with ours

  TOTBWF

  committed
  bc79188

  Copy full SHA for bc79188

• Add a quick helper lemma to coproducts

  TOTBWF

  committed
  593e397

  Copy full SHA for 593e397

• Prove some stuff about biproducts + (co)products

  TOTBWF

  committed
  3b20225

  Copy full SHA for 3b20225

• More Preadditive Properties

  TOTBWF

  committed
  26115b1

  Copy full SHA for 26115b1

• [WIP] Refactor Preadditve properties to use new biproduct

  TOTBWF

  committed
  ee0c8e1

  Copy full SHA for ee0c8e1

Commits on Apr 3, 2021

• [WIP] Normal epimorphisms

  TOTBWF

  committed
  530a67c

  Copy full SHA for 530a67c

• [WIP] A bunch of junk with abelian categories

  TOTBWF

  committed
  84236c6

  Copy full SHA for 84236c6

• Merge remote-tracking branch 'origin/master' into abelian-categories

  TOTBWF

  committed
  2677bdb

  Copy full SHA for 2677bdb

• Merge branch 'abelian-categories' of github.com:TOTBWF/agda-categories into abelian-categories

  TOTBWF

  committed
  b9128b3

  Copy full SHA for b9128b3

• [WIP] Categories of (non-negatively graded) chain complexes

  TOTBWF

  committed
  6fe3c13

  Copy full SHA for 6fe3c13