Code

[WIP] Monoidal Category Tactic#279

Code

Draft

TOTBWF wants to merge 8 commits intoagda:masteragda/agda-categories:masterfrom TOTBWF:monoid-solverTOTBWF/agda-categories:monoid-solverCopy head branch name to clipboard

+451

Commits

Commits on May 4, 2021

• Start work on a monoidal category solver

  TOTBWF

  committed
  e0845b2

  Copy full SHA for e0845b2

• WIP: reworked @TOTBWF's monoid solver.

  sstucki

  committed
  27dc6ad

  Copy full SHA for 27dc6ad

Commits on May 5, 2021

• Merge remote-tracking branch 'sstucki/monoid-solver' into monoid-solver

  TOTBWF

  committed
  7a8e802

  Copy full SHA for 7a8e802

• Prove the ρ⁻¹′ case

  TOTBWF

  committed
  e36b012

  Copy full SHA for e36b012

• Add a ⊗-elim to Monoidal Reasoning

  TOTBWF

  committed
  60ad8f5

  Copy full SHA for 60ad8f5

• Work on the associator case

  TOTBWF

  committed
  e894e16

  Copy full SHA for e894e16

Commits on May 8, 2021

• Finish the proof that normalization respects equality

  TOTBWF

  committed
  dde08b7

  Copy full SHA for dde08b7

• Clean up some proofs

  TOTBWF

  committed
  a10b7d2

  Copy full SHA for a10b7d2