Code

More dagger category theory#420

Code

Merged

JacquesCarette merged 14 commits intomasteragda/agda-categories:masterfrom dagger-functorsagda/agda-categories:dagger-functorsCopy head branch name to clipboardJun 3, 2024

+156-2

Commits

Commits on May 27, 2024

• Definition of dagger functors

  Taneb

  committed
  3040db7

  Copy full SHA for 3040db7

• Dagger functor categories

  Taneb

  committed
  ad70755

  Copy full SHA for ad70755

• Dagger functor dagger categories

  Taneb

  committed
  fe9b960

  Copy full SHA for fe9b960

• Category of dagger categories

  Taneb

  committed
  9730fd3

  Copy full SHA for 9730fd3

Commits on May 28, 2024

• Remove commented out code

  Taneb

  committed
  88a6ad0

  Copy full SHA for 88a6ad0

• Open DaggerFunctor in definition of DagCats

  Taneb

  committed
  529e8ec

  Copy full SHA for 529e8ec

• Restrict imports in Categories.Functor.Dagger

  Taneb

  committed
  d603f7e

  Copy full SHA for d603f7e

• Restrict most of the imports in Categories.Category.Instance.DagCats

  Show description for f84f200
  Taneb

  committed
  f84f200

  Copy full SHA for f84f200

• Restrict imports in Categories.Category.Dagger.Construction.DaggerFunctors

  Taneb

  committed
  5653bd8

  Copy full SHA for 5653bd8

Commits on May 29, 2024

• Only use one †-resp-≈ in commute and sym-commute for dagger functor dagger

  Taneb

  committed
  7470856

  Copy full SHA for 7470856

• Add comment about why not ntHelper

  Taneb

  committed
  d6b02c7

  Copy full SHA for d6b02c7

• Use sym-associator for Cats and DagCats

  Taneb

  committed
  23306c7

  Copy full SHA for 23306c7

• Move dagger for daggerunctors to a where clause

  Taneb

  committed
  9988022

  Copy full SHA for 9988022

• Restrict imports in Categories.Category.Construction.DaggerFunctors

  Taneb

  committed
  7cb0263

  Copy full SHA for 7cb0263