Commit 2019-05-31 17:26 8ebea315

View on Github →

feat(category_theory/monoidal): the monoidal category of types (#1100)

  • feat(category_theory/iso): missing lemmas
  • formatting
  • formatting
  • almost
  • oops
  • getting there
  • one more
  • sleep
  • good to go
  • monoidal category of types
  • fix names
  • renaming
  • linebreak
  • temporary notations
  • notations for associator, unitors?
  • more notation
  • names
  • more names
  • oops
  • renaming, and namespaces
  • comment
  • fix comment
  • remove unnecessary open, formatting
  • removing dsimps
  • replace with simp lemmas
  • fix
  • Update types.lean
  • fix namespace

Estimated changes