Commit 2022-12-04 13:01 8aaf2807

View on Github →

feat: port CategoryTheory.NatIso (#820)

  • feat: port CategoryTheory.NatIso
  • Initial fixes
  • Additional porting notes
  • Update to mathlib4 names
  • Fix lints
  • Swap tidy with aesop
  • Use the correct lowerCamelCase
  • Fix Category.assoc proofs. Explicitly prove ofComponents
  • fix reassoc
  • chore: fix aesop_cat wrapper for aesop
  • .
  • fix reassoc
  • aesop rules
  • cleanup

Estimated changes